Theorem rexralbidv 3228

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wral 3076  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3077  df-rex 3087

This theorem is used by:  freq1  5622  rexfiuz  15436  cau3lem  15443  caubnd2  15446  climi  15598  rlimi  15601  o1lo1  15625  2clim  15660  lo1le  15740  caucvgrlem  15761  caurcvgr  15762  caucvgb  15768  vdwlem10  17083  vdwlem13  17086  pmatcollpw2lem  23003  neiptopnei  23358  lmcvg  23488  lmss  23524  elpt  23799  elptr  23800  txlm  23875  tsmsi  24361  ustuqtop4  24471  isucn  24504  isucn2  24505  ucnima  24507  metcnpi  24771  metcnpi2  24772  metucn  24798  xrge0tsms  25062  elcncf  25118  cncfi  25123  lmmcvg  25490  lhop1  26242  ulmval  26617  ulmi  26623  ulmcaulem  26631  ulmdvlem3  26639  pntibnd  27830  pntlem3  27846  pntleml  27848  axtgcont1  28810  perpln1  29065  perpln2  29066  isperp  29067  brbtwn  29357  uvtx01vtx  29858  isgrpo  30979  ubthlem3  31354  ubth  31355  hcau  31666  hcaucvg  31668  hlimi  31670  hlimconvi  31673  hlim2  31674  elcnop  32339  elcnfn  32364  cnopc  32395  cnfnc  32412  lnopcon  32517  lnfncon  32538  riesz1  32547  xrge0tsmsd  33514  signsply0  35060  unblimceq0  37205  cvgcau  46319  limcleqr  46473  addlimc  46477  0ellimcdiv  46478  climd  46501  climisp  46575  lmbr3  46576  climrescn  46577  climxrrelem  46578  climxrre  46579  xlimpnfxnegmnf  46643  xlimxrre  46660  xlimmnf  46670  xlimpnf  46671  xlimmnfmpt  46672  xlimpnfmpt  46673  dfxlim2  46677  cncfshift  46703  cncfperiod  46708  ioodvbdlimc1lem1  46760  ioodvbdlimc1lem2  46761  ioodvbdlimc2lem  46763  fourierdlem68  47003  fourierdlem87  47022  fourierdlem103  47038  fourierdlem104  47039  etransclem48  47111