Theorem rexralbidv 3221

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3059  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-ral 3060  df-rex 3069

This theorem is referenced by:  freq1  5656  rexfiuz  15383  cau3lem  15390  caubnd2  15393  climi  15543  rlimi  15546  o1lo1  15570  2clim  15605  lo1le  15685  caucvgrlem  15706  caurcvgr  15707  caucvgb  15713  vdwlem10  17024  vdwlem13  17027  pmatcollpw2lem  22799  neiptopnei  23156  lmcvg  23286  lmss  23322  elpt  23596  elptr  23597  txlm  23672  tsmsi  24158  ustuqtop4  24269  isucn  24303  isucn2  24304  ucnima  24306  metcnpi  24573  metcnpi2  24574  metucn  24600  xrge0tsms  24870  elcncf  24929  cncfi  24934  lmmcvg  25309  lhop1  26068  ulmval  26438  ulmi  26444  ulmcaulem  26452  ulmdvlem3  26460  pntibnd  27652  pntlem3  27668  pntleml  27670  axtgcont1  28491  perpln1  28733  perpln2  28734  isperp  28735  brbtwn  28929  uvtx01vtx  29429  isgrpo  30526  ubthlem3  30901  ubth  30902  hcau  31213  hcaucvg  31215  hlimi  31217  hlimconvi  31220  hlim2  31221  elcnop  31886  elcnfn  31911  cnopc  31942  cnfnc  31959  lnopcon  32064  lnfncon  32085  riesz1  32094  xrge0tsmsd  33048  signsply0  34545  unblimceq0  36490  cvgcau  45441  limcleqr  45600  addlimc  45604  0ellimcdiv  45605  climd  45628  climisp  45702  lmbr3  45703  climrescn  45704  climxrrelem  45705  climxrre  45706  xlimpnfxnegmnf  45770  xlimxrre  45787  xlimmnf  45797  xlimpnf  45798  xlimmnfmpt  45799  xlimpnfmpt  45800  dfxlim2  45804  cncfshift  45830  cncfperiod  45835  ioodvbdlimc1lem1  45887  ioodvbdlimc1lem2  45888  ioodvbdlimc2lem  45890  fourierdlem68  46130  fourierdlem87  46149  fourierdlem103  46165  fourierdlem104  46166  etransclem48  46238