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  5586  rexfiuz  15255  cau3lem  15262  caubnd2  15265  climi  15417  rlimi  15420  o1lo1  15444  2clim  15479  lo1le  15559  caucvgrlem  15580  caurcvgr  15581  caucvgb  15587  vdwlem10  16902  vdwlem13  16905  pmatcollpw2lem  22662  neiptopnei  23017  lmcvg  23147  lmss  23183  elpt  23457  elptr  23458  txlm  23533  tsmsi  24019  ustuqtop4  24130  isucn  24163  isucn2  24164  ucnima  24166  metcnpi  24430  metcnpi2  24431  metucn  24457  xrge0tsms  24721  elcncf  24780  cncfi  24785  lmmcvg  25159  lhop1  25917  ulmval  26287  ulmi  26293  ulmcaulem  26301  ulmdvlem3  26309  pntibnd  27502  pntlem3  27518  pntleml  27520  axtgcont1  28413  perpln1  28655  perpln2  28656  isperp  28657  brbtwn  28844  uvtx01vtx  29342  isgrpo  30441  ubthlem3  30816  ubth  30817  hcau  31128  hcaucvg  31130  hlimi  31132  hlimconvi  31135  hlim2  31136  elcnop  31801  elcnfn  31826  cnopc  31857  cnfnc  31874  lnopcon  31979  lnfncon  32000  riesz1  32009  xrge0tsmsd  33015  signsply0  34519  unblimceq0  36485  cvgcau  45473  limcleqr  45629  addlimc  45633  0ellimcdiv  45634  climd  45657  climisp  45731  lmbr3  45732  climrescn  45733  climxrrelem  45734  climxrre  45735  xlimpnfxnegmnf  45799  xlimxrre  45816  xlimmnf  45826  xlimpnf  45827  xlimmnfmpt  45828  xlimpnfmpt  45829  dfxlim2  45833  cncfshift  45859  cncfperiod  45864  ioodvbdlimc1lem1  45916  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  fourierdlem68  46159  fourierdlem87  46178  fourierdlem103  46194  fourierdlem104  46195  etransclem48  46267