Theorem rexralbidv 3230

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3064  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  freq1  5559  rexfiuz  15059  cau3lem  15066  caubnd2  15069  climi  15219  rlimi  15222  o1lo1  15246  2clim  15281  lo1le  15363  caucvgrlem  15384  caurcvgr  15385  caucvgb  15391  vdwlem10  16691  vdwlem13  16694  pmatcollpw2lem  21926  neiptopnei  22283  lmcvg  22413  lmss  22449  elpt  22723  elptr  22724  txlm  22799  tsmsi  23285  ustuqtop4  23396  isucn  23430  isucn2  23431  ucnima  23433  metcnpi  23700  metcnpi2  23701  metucn  23727  xrge0tsms  23997  elcncf  24052  cncfi  24057  lmmcvg  24425  lhop1  25178  ulmval  25539  ulmi  25545  ulmcaulem  25553  ulmdvlem3  25561  pntibnd  26741  pntlem3  26757  pntleml  26759  axtgcont1  26829  perpln1  27071  perpln2  27072  isperp  27073  brbtwn  27267  uvtx01vtx  27764  isgrpo  28859  ubthlem3  29234  ubth  29235  hcau  29546  hcaucvg  29548  hlimi  29550  hlimconvi  29553  hlim2  29554  elcnop  30219  elcnfn  30244  cnopc  30275  cnfnc  30292  lnopcon  30397  lnfncon  30418  riesz1  30427  xrge0tsmsd  31317  signsply0  32530  unblimceq0  34687  limcleqr  43185  addlimc  43189  0ellimcdiv  43190  climd  43213  climisp  43287  lmbr3  43288  climrescn  43289  climxrrelem  43290  climxrre  43291  xlimpnfxnegmnf  43355  xlimxrre  43372  xlimmnf  43382  xlimpnf  43383  xlimmnfmpt  43384  xlimpnfmpt  43385  dfxlim2  43389  cncfshift  43415  cncfperiod  43420  ioodvbdlimc1lem1  43472  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  fourierdlem68  43715  fourierdlem87  43734  fourierdlem103  43750  fourierdlem104  43751  etransclem48  43823