Theorem rexralbidv 3195

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

Hypothesis

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

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

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

Proof of Theorem rexralbidv

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3044  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  freq1  5580  rexfiuz  15242  cau3lem  15249  caubnd2  15252  climi  15404  rlimi  15407  o1lo1  15431  2clim  15466  lo1le  15546  caucvgrlem  15567  caurcvgr  15568  caucvgb  15574  vdwlem10  16889  vdwlem13  16892  pmatcollpw2lem  22646  neiptopnei  23001  lmcvg  23131  lmss  23167  elpt  23441  elptr  23442  txlm  23517  tsmsi  24003  ustuqtop4  24113  isucn  24146  isucn2  24147  ucnima  24149  metcnpi  24413  metcnpi2  24414  metucn  24440  xrge0tsms  24704  elcncf  24763  cncfi  24768  lmmcvg  25142  lhop1  25900  ulmval  26270  ulmi  26276  ulmcaulem  26284  ulmdvlem3  26292  pntibnd  27485  pntlem3  27501  pntleml  27503  axtgcont1  28400  perpln1  28642  perpln2  28643  isperp  28644  brbtwn  28831  uvtx01vtx  29329  isgrpo  30428  ubthlem3  30803  ubth  30804  hcau  31115  hcaucvg  31117  hlimi  31119  hlimconvi  31122  hlim2  31123  elcnop  31788  elcnfn  31813  cnopc  31844  cnfnc  31861  lnopcon  31966  lnfncon  31987  riesz1  31996  xrge0tsmsd  33010  signsply0  34532  unblimceq0  36498  cvgcau  45485  limcleqr  45639  addlimc  45643  0ellimcdiv  45644  climd  45667  climisp  45741  lmbr3  45742  climrescn  45743  climxrrelem  45744  climxrre  45745  xlimpnfxnegmnf  45809  xlimxrre  45826  xlimmnf  45836  xlimpnf  45837  xlimmnfmpt  45838  xlimpnfmpt  45839  dfxlim2  45843  cncfshift  45869  cncfperiod  45874  ioodvbdlimc1lem1  45926  ioodvbdlimc1lem2  45927  ioodvbdlimc2lem  45929  fourierdlem68  46169  fourierdlem87  46188  fourierdlem103  46204  fourierdlem104  46205  etransclem48  46277