Theorem rexralbidv 3220

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3061  ∃wrex 3070

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-ral 3062  df-rex 3071

This theorem is referenced by:  freq1  5645  rexfiuz  15290  cau3lem  15297  caubnd2  15300  climi  15450  rlimi  15453  o1lo1  15477  2clim  15512  lo1le  15594  caucvgrlem  15615  caurcvgr  15616  caucvgb  15622  vdwlem10  16919  vdwlem13  16922  pmatcollpw2lem  22270  neiptopnei  22627  lmcvg  22757  lmss  22793  elpt  23067  elptr  23068  txlm  23143  tsmsi  23629  ustuqtop4  23740  isucn  23774  isucn2  23775  ucnima  23777  metcnpi  24044  metcnpi2  24045  metucn  24071  xrge0tsms  24341  elcncf  24396  cncfi  24401  lmmcvg  24769  lhop1  25522  ulmval  25883  ulmi  25889  ulmcaulem  25897  ulmdvlem3  25905  pntibnd  27085  pntlem3  27101  pntleml  27103  axtgcont1  27708  perpln1  27950  perpln2  27951  isperp  27952  brbtwn  28146  uvtx01vtx  28643  isgrpo  29737  ubthlem3  30112  ubth  30113  hcau  30424  hcaucvg  30426  hlimi  30428  hlimconvi  30431  hlim2  30432  elcnop  31097  elcnfn  31122  cnopc  31153  cnfnc  31170  lnopcon  31275  lnfncon  31296  riesz1  31305  xrge0tsmsd  32196  signsply0  33550  unblimceq0  35371  cvgcau  44187  limcleqr  44346  addlimc  44350  0ellimcdiv  44351  climd  44374  climisp  44448  lmbr3  44449  climrescn  44450  climxrrelem  44451  climxrre  44452  xlimpnfxnegmnf  44516  xlimxrre  44533  xlimmnf  44543  xlimpnf  44544  xlimmnfmpt  44545  xlimpnfmpt  44546  dfxlim2  44550  cncfshift  44576  cncfperiod  44581  ioodvbdlimc1lem1  44633  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  fourierdlem68  44876  fourierdlem87  44895  fourierdlem103  44911  fourierdlem104  44912  etransclem48  44984