Theorem rexralbidv 3228

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wral 3076  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-ral 3077  df-rex 3087

This theorem is referenced by:  freq1  5614  rexfiuz  15375  cau3lem  15382  caubnd2  15385  climi  15537  rlimi  15540  o1lo1  15564  2clim  15599  lo1le  15679  caucvgrlem  15700  caurcvgr  15701  caucvgb  15707  vdwlem10  17026  vdwlem13  17029  pmatcollpw2lem  22837  neiptopnei  23192  lmcvg  23322  lmss  23358  elpt  23632  elptr  23633  txlm  23708  tsmsi  24194  ustuqtop4  24304  isucn  24337  isucn2  24338  ucnima  24340  metcnpi  24604  metcnpi2  24605  metucn  24631  xrge0tsms  24895  elcncf  24951  cncfi  24956  lmmcvg  25323  lhop1  26076  ulmval  26443  ulmi  26449  ulmcaulem  26457  ulmdvlem3  26465  pntibnd  27657  pntlem3  27673  pntleml  27675  axtgcont1  28637  perpln1  28883  perpln2  28884  isperp  28885  brbtwn  29100  uvtx01vtx  29598  isgrpo  30700  ubthlem3  31075  ubth  31076  hcau  31387  hcaucvg  31389  hlimi  31391  hlimconvi  31394  hlim2  31395  elcnop  32060  elcnfn  32085  cnopc  32116  cnfnc  32133  lnopcon  32238  lnfncon  32259  riesz1  32268  xrge0tsmsd  33253  signsply0  34845  unblimceq0  36945  cvgcau  46064  limcleqr  46218  addlimc  46222  0ellimcdiv  46223  climd  46246  climisp  46320  lmbr3  46321  climrescn  46322  climxrrelem  46323  climxrre  46324  xlimpnfxnegmnf  46388  xlimxrre  46405  xlimmnf  46415  xlimpnf  46416  xlimmnfmpt  46417  xlimpnfmpt  46418  dfxlim2  46422  cncfshift  46448  cncfperiod  46453  ioodvbdlimc1lem1  46505  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  fourierdlem68  46748  fourierdlem87  46767  fourierdlem103  46783  fourierdlem104  46784  etransclem48  46856