Theorem rexralbidv 3205

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wral 3053  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3054  df-rex 3064

This theorem is referenced by:  freq1  5585  rexfiuz  15301  cau3lem  15308  caubnd2  15311  climi  15463  rlimi  15466  o1lo1  15490  2clim  15525  lo1le  15605  caucvgrlem  15626  caurcvgr  15627  caucvgb  15633  vdwlem10  16952  vdwlem13  16955  pmatcollpw2lem  22760  neiptopnei  23115  lmcvg  23245  lmss  23281  elpt  23555  elptr  23556  txlm  23631  tsmsi  24117  ustuqtop4  24227  isucn  24260  isucn2  24261  ucnima  24263  metcnpi  24527  metcnpi2  24528  metucn  24554  xrge0tsms  24818  elcncf  24874  cncfi  24879  lmmcvg  25246  lhop1  25999  ulmval  26363  ulmi  26369  ulmcaulem  26377  ulmdvlem3  26385  pntibnd  27574  pntlem3  27590  pntleml  27592  axtgcont1  28554  perpln1  28796  perpln2  28797  isperp  28798  brbtwn  28986  uvtx01vtx  29484  isgrpo  30586  ubthlem3  30961  ubth  30962  hcau  31273  hcaucvg  31275  hlimi  31277  hlimconvi  31280  hlim2  31281  elcnop  31946  elcnfn  31971  cnopc  32002  cnfnc  32019  lnopcon  32124  lnfncon  32145  riesz1  32154  xrge0tsmsd  33154  signsply0  34735  unblimceq0  36813  cvgcau  45933  limcleqr  46087  addlimc  46091  0ellimcdiv  46092  climd  46115  climisp  46189  lmbr3  46190  climrescn  46191  climxrrelem  46192  climxrre  46193  xlimpnfxnegmnf  46257  xlimxrre  46274  xlimmnf  46284  xlimpnf  46285  xlimmnfmpt  46286  xlimpnfmpt  46287  dfxlim2  46291  cncfshift  46317  cncfperiod  46322  ioodvbdlimc1lem1  46374  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  fourierdlem68  46617  fourierdlem87  46636  fourierdlem103  46652  fourierdlem104  46653  etransclem48  46725