Theorem rexralbidv 3304

Description: Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2rexbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexralbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem rexralbidv

Step	Hyp	Ref	Expression
1		2rexbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ralbidv 3200	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3300	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 208  ∀wral 3141  ∃wrex 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-ral 3146  df-rex 3147

This theorem is referenced by:  freq1  5528  rexfiuz  14710  cau3lem  14717  caubnd2  14720  climi  14870  rlimi  14873  o1lo1  14897  2clim  14932  lo1le  15011  caucvgrlem  15032  caurcvgr  15033  caucvgb  15039  vdwlem10  16329  vdwlem13  16332  pmatcollpw2lem  21388  neiptopnei  21743  lmcvg  21873  lmss  21909  elpt  22183  elptr  22184  txlm  22259  tsmsi  22745  ustuqtop4  22856  isucn  22890  isucn2  22891  ucnima  22893  metcnpi  23157  metcnpi2  23158  metucn  23184  xrge0tsms  23445  elcncf  23500  cncfi  23505  lmmcvg  23867  lhop1  24614  ulmval  24971  ulmi  24977  ulmcaulem  24985  ulmdvlem3  24993  pntibnd  26172  pntlem3  26188  pntleml  26190  axtgcont1  26257  perpln1  26499  perpln2  26500  isperp  26501  brbtwn  26688  uvtx01vtx  27182  isgrpo  28277  ubthlem3  28652  ubth  28653  hcau  28964  hcaucvg  28966  hlimi  28968  hlimconvi  28971  hlim2  28972  elcnop  29637  elcnfn  29662  cnopc  29693  cnfnc  29710  lnopcon  29815  lnfncon  29836  riesz1  29845  xrge0tsmsd  30696  signsply0  31825  unblimceq0  33850  limcleqr  41931  addlimc  41935  0ellimcdiv  41936  climd  41959  climisp  42033  lmbr3  42034  climrescn  42035  climxrrelem  42036  climxrre  42037  xlimpnfxnegmnf  42101  xlimxrre  42118  xlimmnf  42128  xlimpnf  42129  xlimmnfmpt  42130  xlimpnfmpt  42131  dfxlim2  42135  cncfshift  42163  cncfperiod  42168  ioodvbdlimc1lem1  42222  ioodvbdlimc1lem2  42223  ioodvbdlimc2lem  42225  fourierdlem68  42466  fourierdlem87  42485  fourierdlem103  42501  fourierdlem104  42502  etransclem48  42574