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 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  freq1  5618  rexfiuz  15524  cau3lem  15531  caubnd2  15534  climi  15686  rlimi  15689  o1lo1  15713  2clim  15748  lo1le  15828  caucvgrlem  15849  caurcvgr  15850  caucvgb  15856  vdwlem10  17177  vdwlem13  17180  pmatcollpw2lem  23104  neiptopnei  23459  lmcvg  23589  lmss  23625  elpt  23900  elptr  23901  txlm  23976  tsmsi  24462  ustuqtop4  24572  isucn  24605  isucn2  24606  ucnima  24608  metcnpi  24872  metcnpi2  24873  metucn  24899  xrge0tsms  25163  elcncf  25219  cncfi  25224  lmmcvg  25591  lhop1  26343  ulmval  26716  ulmi  26722  ulmcaulem  26730  ulmdvlem3  26738  pntibnd  27929  pntlem3  27945  pntleml  27947  axtgcont1  28939  perpln1  29194  perpln2  29195  isperp  29196  brbtwn  29486  uvtx01vtx  29987  isgrpo  31108  ubthlem3  31483  ubth  31484  hcau  31795  hcaucvg  31797  hlimi  31799  hlimconvi  31802  hlim2  31803  elcnop  32468  elcnfn  32493  cnopc  32524  cnfnc  32541  lnopcon  32646  lnfncon  32667  riesz1  32676  xrge0tsmsd  33684  signsply0  35230  srepdf  36038  unblimceq0  37497  cvgcau  46636  limcleqr  46790  addlimc  46794  0ellimcdiv  46795  climd  46818  climisp  46892  lmbr3  46893  climrescn  46894  climxrrelem  46895  climxrre  46896  xlimpnfxnegmnf  46960  xlimxrre  46977  xlimmnf  46987  xlimpnf  46988  xlimmnfmpt  46989  xlimpnfmpt  46990  dfxlim2  46994  cncfshift  47020  cncfperiod  47025  ioodvbdlimc1lem1  47077  ioodvbdlimc1lem2  47078  ioodvbdlimc2lem  47080  fourierdlem68  47320  fourierdlem87  47339  fourierdlem103  47355  fourierdlem104  47356  etransclem48  47428