Theorem rexralbidv 3229

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3067  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-ral 3068  df-rex 3077

This theorem is referenced by:  freq1  5667  rexfiuz  15396  cau3lem  15403  caubnd2  15406  climi  15556  rlimi  15559  o1lo1  15583  2clim  15618  lo1le  15700  caucvgrlem  15721  caurcvgr  15722  caucvgb  15728  vdwlem10  17037  vdwlem13  17040  pmatcollpw2lem  22804  neiptopnei  23161  lmcvg  23291  lmss  23327  elpt  23601  elptr  23602  txlm  23677  tsmsi  24163  ustuqtop4  24274  isucn  24308  isucn2  24309  ucnima  24311  metcnpi  24578  metcnpi2  24579  metucn  24605  xrge0tsms  24875  elcncf  24934  cncfi  24939  lmmcvg  25314  lhop1  26073  ulmval  26441  ulmi  26447  ulmcaulem  26455  ulmdvlem3  26463  pntibnd  27655  pntlem3  27671  pntleml  27673  axtgcont1  28494  perpln1  28736  perpln2  28737  isperp  28738  brbtwn  28932  uvtx01vtx  29432  isgrpo  30529  ubthlem3  30904  ubth  30905  hcau  31216  hcaucvg  31218  hlimi  31220  hlimconvi  31223  hlim2  31224  elcnop  31889  elcnfn  31914  cnopc  31945  cnfnc  31962  lnopcon  32067  lnfncon  32088  riesz1  32097  xrge0tsmsd  33041  signsply0  34528  unblimceq0  36473  cvgcau  45406  limcleqr  45565  addlimc  45569  0ellimcdiv  45570  climd  45593  climisp  45667  lmbr3  45668  climrescn  45669  climxrrelem  45670  climxrre  45671  xlimpnfxnegmnf  45735  xlimxrre  45752  xlimmnf  45762  xlimpnf  45763  xlimmnfmpt  45764  xlimpnfmpt  45765  dfxlim2  45769  cncfshift  45795  cncfperiod  45800  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  fourierdlem68  46095  fourierdlem87  46114  fourierdlem103  46130  fourierdlem104  46131  etransclem48  46203