Theorem rexralbidv 3229

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  freq1  5550  rexfiuz  14987  cau3lem  14994  caubnd2  14997  climi  15147  rlimi  15150  o1lo1  15174  2clim  15209  lo1le  15291  caucvgrlem  15312  caurcvgr  15313  caucvgb  15319  vdwlem10  16619  vdwlem13  16622  pmatcollpw2lem  21834  neiptopnei  22191  lmcvg  22321  lmss  22357  elpt  22631  elptr  22632  txlm  22707  tsmsi  23193  ustuqtop4  23304  isucn  23338  isucn2  23339  ucnima  23341  metcnpi  23606  metcnpi2  23607  metucn  23633  xrge0tsms  23903  elcncf  23958  cncfi  23963  lmmcvg  24330  lhop1  25083  ulmval  25444  ulmi  25450  ulmcaulem  25458  ulmdvlem3  25466  pntibnd  26646  pntlem3  26662  pntleml  26664  axtgcont1  26733  perpln1  26975  perpln2  26976  isperp  26977  brbtwn  27170  uvtx01vtx  27667  isgrpo  28760  ubthlem3  29135  ubth  29136  hcau  29447  hcaucvg  29449  hlimi  29451  hlimconvi  29454  hlim2  29455  elcnop  30120  elcnfn  30145  cnopc  30176  cnfnc  30193  lnopcon  30298  lnfncon  30319  riesz1  30328  xrge0tsmsd  31219  signsply0  32430  unblimceq0  34614  limcleqr  43075  addlimc  43079  0ellimcdiv  43080  climd  43103  climisp  43177  lmbr3  43178  climrescn  43179  climxrrelem  43180  climxrre  43181  xlimpnfxnegmnf  43245  xlimxrre  43262  xlimmnf  43272  xlimpnf  43273  xlimmnfmpt  43274  xlimpnfmpt  43275  dfxlim2  43279  cncfshift  43305  cncfperiod  43310  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  fourierdlem68  43605  fourierdlem87  43624  fourierdlem103  43640  fourierdlem104  43641  etransclem48  43713