Theorem rexralbidv 3200

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3049  ∃wrex 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3050  df-rex 3059

This theorem is referenced by:  freq1  5589  rexfiuz  15269  cau3lem  15276  caubnd2  15279  climi  15431  rlimi  15434  o1lo1  15458  2clim  15493  lo1le  15573  caucvgrlem  15594  caurcvgr  15595  caucvgb  15601  vdwlem10  16916  vdwlem13  16919  pmatcollpw2lem  22719  neiptopnei  23074  lmcvg  23204  lmss  23240  elpt  23514  elptr  23515  txlm  23590  tsmsi  24076  ustuqtop4  24186  isucn  24219  isucn2  24220  ucnima  24222  metcnpi  24486  metcnpi2  24487  metucn  24513  xrge0tsms  24777  elcncf  24836  cncfi  24841  lmmcvg  25215  lhop1  25973  ulmval  26343  ulmi  26349  ulmcaulem  26357  ulmdvlem3  26365  pntibnd  27558  pntlem3  27574  pntleml  27576  axtgcont1  28489  perpln1  28731  perpln2  28732  isperp  28733  brbtwn  28921  uvtx01vtx  29419  isgrpo  30521  ubthlem3  30896  ubth  30897  hcau  31208  hcaucvg  31210  hlimi  31212  hlimconvi  31215  hlim2  31216  elcnop  31881  elcnfn  31906  cnopc  31937  cnfnc  31954  lnopcon  32059  lnfncon  32080  riesz1  32089  xrge0tsmsd  33104  signsply0  34657  unblimceq0  36650  cvgcau  45676  limcleqr  45830  addlimc  45834  0ellimcdiv  45835  climd  45858  climisp  45932  lmbr3  45933  climrescn  45934  climxrrelem  45935  climxrre  45936  xlimpnfxnegmnf  46000  xlimxrre  46017  xlimmnf  46027  xlimpnf  46028  xlimmnfmpt  46029  xlimpnfmpt  46030  dfxlim2  46034  cncfshift  46060  cncfperiod  46065  ioodvbdlimc1lem1  46117  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  fourierdlem68  46360  fourierdlem87  46379  fourierdlem103  46395  fourierdlem104  46396  etransclem48  46468