Theorem rexralbidv 3226

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wral 3071  ∃wrex 3072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-ral 3076  df-rex 3077

This theorem is referenced by:  freq1  5495  rexfiuz  14756  cau3lem  14763  caubnd2  14766  climi  14916  rlimi  14919  o1lo1  14943  2clim  14978  lo1le  15057  caucvgrlem  15078  caurcvgr  15079  caucvgb  15085  vdwlem10  16382  vdwlem13  16385  pmatcollpw2lem  21478  neiptopnei  21833  lmcvg  21963  lmss  21999  elpt  22273  elptr  22274  txlm  22349  tsmsi  22835  ustuqtop4  22946  isucn  22980  isucn2  22981  ucnima  22983  metcnpi  23247  metcnpi2  23248  metucn  23274  xrge0tsms  23536  elcncf  23591  cncfi  23596  lmmcvg  23962  lhop1  24714  ulmval  25075  ulmi  25081  ulmcaulem  25089  ulmdvlem3  25097  pntibnd  26277  pntlem3  26293  pntleml  26295  axtgcont1  26362  perpln1  26604  perpln2  26605  isperp  26606  brbtwn  26793  uvtx01vtx  27287  isgrpo  28380  ubthlem3  28755  ubth  28756  hcau  29067  hcaucvg  29069  hlimi  29071  hlimconvi  29074  hlim2  29075  elcnop  29740  elcnfn  29765  cnopc  29796  cnfnc  29813  lnopcon  29918  lnfncon  29939  riesz1  29948  xrge0tsmsd  30844  signsply0  32050  unblimceq0  34237  limcleqr  42653  addlimc  42657  0ellimcdiv  42658  climd  42681  climisp  42755  lmbr3  42756  climrescn  42757  climxrrelem  42758  climxrre  42759  xlimpnfxnegmnf  42823  xlimxrre  42840  xlimmnf  42850  xlimpnf  42851  xlimmnfmpt  42852  xlimpnfmpt  42853  dfxlim2  42857  cncfshift  42883  cncfperiod  42888  ioodvbdlimc1lem1  42940  ioodvbdlimc1lem2  42941  ioodvbdlimc2lem  42943  fourierdlem68  43183  fourierdlem87  43202  fourierdlem103  43218  fourierdlem104  43219  etransclem48  43291