Theorem rexralbidv 3215

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-ral 3055  df-rex 3064

This theorem is referenced by:  freq1  5654  rexfiuz  15366  cau3lem  15373  caubnd2  15376  climi  15526  rlimi  15529  o1lo1  15553  2clim  15588  lo1le  15670  caucvgrlem  15691  caurcvgr  15692  caucvgb  15698  vdwlem10  17006  vdwlem13  17009  pmatcollpw2lem  22771  neiptopnei  23128  lmcvg  23258  lmss  23294  elpt  23568  elptr  23569  txlm  23644  tsmsi  24130  ustuqtop4  24241  isucn  24275  isucn2  24276  ucnima  24278  metcnpi  24545  metcnpi2  24546  metucn  24572  xrge0tsms  24842  elcncf  24901  cncfi  24906  lmmcvg  25281  lhop1  26039  ulmval  26407  ulmi  26413  ulmcaulem  26421  ulmdvlem3  26429  pntibnd  27620  pntlem3  27636  pntleml  27638  axtgcont1  28438  perpln1  28680  perpln2  28681  isperp  28682  brbtwn  28876  uvtx01vtx  29376  isgrpo  30473  ubthlem3  30848  ubth  30849  hcau  31160  hcaucvg  31162  hlimi  31164  hlimconvi  31167  hlim2  31168  elcnop  31833  elcnfn  31858  cnopc  31889  cnfnc  31906  lnopcon  32011  lnfncon  32032  riesz1  32041  xrge0tsmsd  32987  signsply0  34474  unblimceq0  36297  cvgcau  45220  limcleqr  45379  addlimc  45383  0ellimcdiv  45384  climd  45407  climisp  45481  lmbr3  45482  climrescn  45483  climxrrelem  45484  climxrre  45485  xlimpnfxnegmnf  45549  xlimxrre  45566  xlimmnf  45576  xlimpnf  45577  xlimmnfmpt  45578  xlimpnfmpt  45579  dfxlim2  45583  cncfshift  45609  cncfperiod  45614  ioodvbdlimc1lem1  45666  ioodvbdlimc1lem2  45667  ioodvbdlimc2lem  45669  fourierdlem68  45909  fourierdlem87  45928  fourierdlem103  45944  fourierdlem104  45945  etransclem48  46017