Theorem rexralbidv 3237

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wral 3085  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-ral 3086  df-rex 3096

This theorem is referenced by:  freq1  5629  rexfiuz  15398  cau3lem  15405  caubnd2  15408  climi  15560  rlimi  15563  o1lo1  15587  2clim  15622  lo1le  15702  caucvgrlem  15723  caurcvgr  15724  caucvgb  15730  vdwlem10  17049  vdwlem13  17052  pmatcollpw2lem  22902  neiptopnei  23257  lmcvg  23387  lmss  23423  elpt  23697  elptr  23698  txlm  23773  tsmsi  24259  ustuqtop4  24369  isucn  24402  isucn2  24403  ucnima  24405  metcnpi  24669  metcnpi2  24670  metucn  24696  xrge0tsms  24960  elcncf  25016  cncfi  25021  lmmcvg  25388  lhop1  26141  ulmval  26508  ulmi  26514  ulmcaulem  26522  ulmdvlem3  26530  pntibnd  27722  pntlem3  27738  pntleml  27740  axtgcont1  28702  perpln1  28948  perpln2  28949  isperp  28950  brbtwn  29189  uvtx01vtx  29687  isgrpo  30789  ubthlem3  31164  ubth  31165  hcau  31476  hcaucvg  31478  hlimi  31480  hlimconvi  31483  hlim2  31484  elcnop  32149  elcnfn  32174  cnopc  32205  cnfnc  32222  lnopcon  32327  lnfncon  32348  riesz1  32357  xrge0tsmsd  33333  signsply0  34882  unblimceq0  36984  cvgcau  46095  limcleqr  46249  addlimc  46253  0ellimcdiv  46254  climd  46277  climisp  46351  lmbr3  46352  climrescn  46353  climxrrelem  46354  climxrre  46355  xlimpnfxnegmnf  46419  xlimxrre  46436  xlimmnf  46446  xlimpnf  46447  xlimmnfmpt  46448  xlimpnfmpt  46449  dfxlim2  46453  cncfshift  46479  cncfperiod  46484  ioodvbdlimc1lem1  46536  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  fourierdlem68  46779  fourierdlem87  46798  fourierdlem103  46814  fourierdlem104  46815  etransclem48  46887