Theorem rexralbidv 3058

Description: Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2rexbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexralbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem rexralbidv

Step	Hyp	Ref	Expression
1		2rexbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ralbidv 2986	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3052	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 196  ∀wral 2912  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  freq1  5084  rexfiuz  14087  cau3lem  14094  caubnd2  14097  climi  14241  rlimi  14244  o1lo1  14268  2clim  14303  lo1le  14382  caucvgrlem  14403  caurcvgr  14404  caucvgb  14410  vdwlem10  15694  vdwlem13  15697  pmatcollpw2lem  20582  neiptopnei  20936  lmcvg  21066  lmss  21102  elpt  21375  elptr  21376  txlm  21451  tsmsi  21937  ustuqtop4  22048  isucn  22082  isucn2  22083  ucnima  22085  metcnpi  22349  metcnpi2  22350  metucn  22376  xrge0tsms  22637  elcncf  22692  cncfi  22697  lmmcvg  23059  lhop1  23777  ulmval  24134  ulmi  24140  ulmcaulem  24148  ulmdvlem3  24156  pntibnd  25282  pntlem3  25298  pntleml  25300  axtgcont1  25367  perpln1  25605  perpln2  25606  isperp  25607  brbtwn  25779  isgrpo  27351  ubthlem3  27728  ubth  27729  hcau  28041  hcaucvg  28043  hlimi  28045  hlimconvi  28048  hlim2  28049  elcnop  28716  elcnfn  28741  cnopc  28772  cnfnc  28789  lnopcon  28894  lnfncon  28915  riesz1  28924  xrge0tsmsd  29785  signsply0  30628  limcleqr  39876  addlimc  39880  0ellimcdiv  39881  climd  39904  climisp  39978  lmbr3  39979  climrescn  39980  climxrrelem  39981  climxrre  39982  xlimxrre  40057  xlimmnf  40067  xlimpnf  40068  xlimmnfmpt  40069  xlimpnfmpt  40070  dfxlim2  40074  cncfshift  40087  cncfperiod  40092  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  fourierdlem68  40391  fourierdlem87  40410  fourierdlem103  40426  fourierdlem104  40427  etransclem48  40499