Theorem rexralbidv 3233

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 3190	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3191	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wral 3081  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3082  df-rex 3092

This theorem is used by:  freq1  5630  rexfiuz  15425  cau3lem  15432  caubnd2  15435  climi  15587  rlimi  15590  o1lo1  15614  2clim  15649  lo1le  15729  caucvgrlem  15750  caurcvgr  15751  caucvgb  15757  vdwlem10  17074  vdwlem13  17077  pmatcollpw2lem  22986  neiptopnei  23341  lmcvg  23471  lmss  23507  elpt  23782  elptr  23783  txlm  23858  tsmsi  24344  ustuqtop4  24454  isucn  24487  isucn2  24488  ucnima  24490  metcnpi  24754  metcnpi2  24755  metucn  24781  xrge0tsms  25045  elcncf  25101  cncfi  25106  lmmcvg  25473  lhop1  26226  ulmval  26596  ulmi  26602  ulmcaulem  26610  ulmdvlem3  26618  pntibnd  27810  pntlem3  27826  pntleml  27828  axtgcont1  28790  perpln1  29043  perpln2  29044  isperp  29045  brbtwn  29306  uvtx01vtx  29807  isgrpo  30922  ubthlem3  31297  ubth  31298  hcau  31609  hcaucvg  31611  hlimi  31613  hlimconvi  31616  hlim2  31617  elcnop  32282  elcnfn  32307  cnopc  32338  cnfnc  32355  lnopcon  32460  lnfncon  32481  riesz1  32490  xrge0tsmsd  33459  signsply0  35005  unblimceq0  37155  cvgcau  46264  limcleqr  46418  addlimc  46422  0ellimcdiv  46423  climd  46446  climisp  46520  lmbr3  46521  climrescn  46522  climxrrelem  46523  climxrre  46524  xlimpnfxnegmnf  46588  xlimxrre  46605  xlimmnf  46615  xlimpnf  46616  xlimmnfmpt  46617  xlimpnfmpt  46618  dfxlim2  46622  cncfshift  46648  cncfperiod  46653  ioodvbdlimc1lem1  46705  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  fourierdlem68  46948  fourierdlem87  46967  fourierdlem103  46983  fourierdlem104  46984  etransclem48  47056