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  15399  cau3lem  15406  caubnd2  15409  climi  15561  rlimi  15564  o1lo1  15588  2clim  15623  lo1le  15703  caucvgrlem  15724  caurcvgr  15725  caucvgb  15731  vdwlem10  17050  vdwlem13  17053  pmatcollpw2lem  22903  neiptopnei  23258  lmcvg  23388  lmss  23424  elpt  23698  elptr  23699  txlm  23774  tsmsi  24260  ustuqtop4  24370  isucn  24403  isucn2  24404  ucnima  24406  metcnpi  24670  metcnpi2  24671  metucn  24697  xrge0tsms  24961  elcncf  25017  cncfi  25022  lmmcvg  25389  lhop1  26142  ulmval  26509  ulmi  26515  ulmcaulem  26523  ulmdvlem3  26531  pntibnd  27723  pntlem3  27739  pntleml  27741  axtgcont1  28703  perpln1  28949  perpln2  28950  isperp  28951  brbtwn  29190  uvtx01vtx  29688  isgrpo  30790  ubthlem3  31165  ubth  31166  hcau  31477  hcaucvg  31479  hlimi  31481  hlimconvi  31484  hlim2  31485  elcnop  32150  elcnfn  32175  cnopc  32206  cnfnc  32223  lnopcon  32328  lnfncon  32349  riesz1  32358  xrge0tsmsd  33334  signsply0  34883  unblimceq0  36985  cvgcau  46096  limcleqr  46250  addlimc  46254  0ellimcdiv  46255  climd  46278  climisp  46352  lmbr3  46353  climrescn  46354  climxrrelem  46355  climxrre  46356  xlimpnfxnegmnf  46420  xlimxrre  46437  xlimmnf  46447  xlimpnf  46448  xlimmnfmpt  46449  xlimpnfmpt  46450  dfxlim2  46454  cncfshift  46480  cncfperiod  46485  ioodvbdlimc1lem1  46537  ioodvbdlimc1lem2  46538  ioodvbdlimc2lem  46540  fourierdlem68  46780  fourierdlem87  46799  fourierdlem103  46815  fourierdlem104  46816  etransclem48  46888