Theorem rexralbidv 3202

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3051  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3052  df-rex 3061

This theorem is referenced by:  freq1  5591  rexfiuz  15271  cau3lem  15278  caubnd2  15281  climi  15433  rlimi  15436  o1lo1  15460  2clim  15495  lo1le  15575  caucvgrlem  15596  caurcvgr  15597  caucvgb  15603  vdwlem10  16918  vdwlem13  16921  pmatcollpw2lem  22721  neiptopnei  23076  lmcvg  23206  lmss  23242  elpt  23516  elptr  23517  txlm  23592  tsmsi  24078  ustuqtop4  24188  isucn  24221  isucn2  24222  ucnima  24224  metcnpi  24488  metcnpi2  24489  metucn  24515  xrge0tsms  24779  elcncf  24838  cncfi  24843  lmmcvg  25217  lhop1  25975  ulmval  26345  ulmi  26351  ulmcaulem  26359  ulmdvlem3  26367  pntibnd  27560  pntlem3  27576  pntleml  27578  axtgcont1  28540  perpln1  28782  perpln2  28783  isperp  28784  brbtwn  28972  uvtx01vtx  29470  isgrpo  30572  ubthlem3  30947  ubth  30948  hcau  31259  hcaucvg  31261  hlimi  31263  hlimconvi  31266  hlim2  31267  elcnop  31932  elcnfn  31957  cnopc  31988  cnfnc  32005  lnopcon  32110  lnfncon  32131  riesz1  32140  xrge0tsmsd  33155  signsply0  34708  unblimceq0  36707  cvgcau  45744  limcleqr  45898  addlimc  45902  0ellimcdiv  45903  climd  45926  climisp  46000  lmbr3  46001  climrescn  46002  climxrrelem  46003  climxrre  46004  xlimpnfxnegmnf  46068  xlimxrre  46085  xlimmnf  46095  xlimpnf  46096  xlimmnfmpt  46097  xlimpnfmpt  46098  dfxlim2  46102  cncfshift  46128  cncfperiod  46133  ioodvbdlimc1lem1  46185  ioodvbdlimc1lem2  46186  ioodvbdlimc2lem  46188  fourierdlem68  46428  fourierdlem87  46447  fourierdlem103  46463  fourierdlem104  46464  etransclem48  46536