Theorem rexralbidv 3301

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wral 3138  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3143  df-rex 3144

This theorem is referenced by:  freq1  5525  rexfiuz  14707  cau3lem  14714  caubnd2  14717  climi  14867  rlimi  14870  o1lo1  14894  2clim  14929  lo1le  15008  caucvgrlem  15029  caurcvgr  15030  caucvgb  15036  vdwlem10  16326  vdwlem13  16329  pmatcollpw2lem  21385  neiptopnei  21740  lmcvg  21870  lmss  21906  elpt  22180  elptr  22181  txlm  22256  tsmsi  22742  ustuqtop4  22853  isucn  22887  isucn2  22888  ucnima  22890  metcnpi  23154  metcnpi2  23155  metucn  23181  xrge0tsms  23442  elcncf  23497  cncfi  23502  lmmcvg  23864  lhop1  24611  ulmval  24968  ulmi  24974  ulmcaulem  24982  ulmdvlem3  24990  pntibnd  26169  pntlem3  26185  pntleml  26187  axtgcont1  26254  perpln1  26496  perpln2  26497  isperp  26498  brbtwn  26685  uvtx01vtx  27179  isgrpo  28274  ubthlem3  28649  ubth  28650  hcau  28961  hcaucvg  28963  hlimi  28965  hlimconvi  28968  hlim2  28969  elcnop  29634  elcnfn  29659  cnopc  29690  cnfnc  29707  lnopcon  29812  lnfncon  29833  riesz1  29842  xrge0tsmsd  30692  signsply0  31821  unblimceq0  33846  limcleqr  41945  addlimc  41949  0ellimcdiv  41950  climd  41973  climisp  42047  lmbr3  42048  climrescn  42049  climxrrelem  42050  climxrre  42051  xlimpnfxnegmnf  42115  xlimxrre  42132  xlimmnf  42142  xlimpnf  42143  xlimmnfmpt  42144  xlimpnfmpt  42145  dfxlim2  42149  cncfshift  42177  cncfperiod  42182  ioodvbdlimc1lem1  42236  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  fourierdlem68  42479  fourierdlem87  42498  fourierdlem103  42514  fourierdlem104  42515  etransclem48  42587