Theorem rexralbidv 3203

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

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

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 3052  df-rex 3062

This theorem is referenced by:  freq1  5598  rexfiuz  15310  cau3lem  15317  caubnd2  15320  climi  15472  rlimi  15475  o1lo1  15499  2clim  15534  lo1le  15614  caucvgrlem  15635  caurcvgr  15636  caucvgb  15642  vdwlem10  16961  vdwlem13  16964  pmatcollpw2lem  22742  neiptopnei  23097  lmcvg  23227  lmss  23263  elpt  23537  elptr  23538  txlm  23613  tsmsi  24099  ustuqtop4  24209  isucn  24242  isucn2  24243  ucnima  24245  metcnpi  24509  metcnpi2  24510  metucn  24536  xrge0tsms  24800  elcncf  24856  cncfi  24861  lmmcvg  25228  lhop1  25981  ulmval  26345  ulmi  26351  ulmcaulem  26359  ulmdvlem3  26367  pntibnd  27556  pntlem3  27572  pntleml  27574  axtgcont1  28536  perpln1  28778  perpln2  28779  isperp  28780  brbtwn  28968  uvtx01vtx  29466  isgrpo  30568  ubthlem3  30943  ubth  30944  hcau  31255  hcaucvg  31257  hlimi  31259  hlimconvi  31262  hlim2  31263  elcnop  31928  elcnfn  31953  cnopc  31984  cnfnc  32001  lnopcon  32106  lnfncon  32127  riesz1  32136  xrge0tsmsd  33134  signsply0  34695  unblimceq0  36767  cvgcau  45918  limcleqr  46072  addlimc  46076  0ellimcdiv  46077  climd  46100  climisp  46174  lmbr3  46175  climrescn  46176  climxrrelem  46177  climxrre  46178  xlimpnfxnegmnf  46242  xlimxrre  46259  xlimmnf  46269  xlimpnf  46270  xlimmnfmpt  46271  xlimpnfmpt  46272  dfxlim2  46276  cncfshift  46302  cncfperiod  46307  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  fourierdlem68  46602  fourierdlem87  46621  fourierdlem103  46637  fourierdlem104  46638  etransclem48  46710