Theorem rexralbidv 3204

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3052  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053  df-rex 3063

This theorem is referenced by:  freq1  5592  rexfiuz  15304  cau3lem  15311  caubnd2  15314  climi  15466  rlimi  15469  o1lo1  15493  2clim  15528  lo1le  15608  caucvgrlem  15629  caurcvgr  15630  caucvgb  15636  vdwlem10  16955  vdwlem13  16958  pmatcollpw2lem  22755  neiptopnei  23110  lmcvg  23240  lmss  23276  elpt  23550  elptr  23551  txlm  23626  tsmsi  24112  ustuqtop4  24222  isucn  24255  isucn2  24256  ucnima  24258  metcnpi  24522  metcnpi2  24523  metucn  24549  xrge0tsms  24813  elcncf  24869  cncfi  24874  lmmcvg  25241  lhop1  25994  ulmval  26361  ulmi  26367  ulmcaulem  26375  ulmdvlem3  26383  pntibnd  27573  pntlem3  27589  pntleml  27591  axtgcont1  28553  perpln1  28795  perpln2  28796  isperp  28797  brbtwn  28985  uvtx01vtx  29483  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  33152  signsply0  34714  unblimceq0  36786  cvgcau  45939  limcleqr  46093  addlimc  46097  0ellimcdiv  46098  climd  46121  climisp  46195  lmbr3  46196  climrescn  46197  climxrrelem  46198  climxrre  46199  xlimpnfxnegmnf  46263  xlimxrre  46280  xlimmnf  46290  xlimpnf  46291  xlimmnfmpt  46292  xlimpnfmpt  46293  dfxlim2  46297  cncfshift  46323  cncfperiod  46328  ioodvbdlimc1lem1  46380  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  fourierdlem68  46623  fourierdlem87  46642  fourierdlem103  46658  fourierdlem104  46659  etransclem48  46731