Theorem rexralbidv 3210

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3060  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-ral 3061  df-rex 3070

This theorem is referenced by:  freq1  5608  rexfiuz  15244  cau3lem  15251  caubnd2  15254  climi  15404  rlimi  15407  o1lo1  15431  2clim  15466  lo1le  15548  caucvgrlem  15569  caurcvgr  15570  caucvgb  15576  vdwlem10  16873  vdwlem13  16876  pmatcollpw2lem  22163  neiptopnei  22520  lmcvg  22650  lmss  22686  elpt  22960  elptr  22961  txlm  23036  tsmsi  23522  ustuqtop4  23633  isucn  23667  isucn2  23668  ucnima  23670  metcnpi  23937  metcnpi2  23938  metucn  23964  xrge0tsms  24234  elcncf  24289  cncfi  24294  lmmcvg  24662  lhop1  25415  ulmval  25776  ulmi  25782  ulmcaulem  25790  ulmdvlem3  25798  pntibnd  26978  pntlem3  26994  pntleml  26996  axtgcont1  27473  perpln1  27715  perpln2  27716  isperp  27717  brbtwn  27911  uvtx01vtx  28408  isgrpo  29502  ubthlem3  29877  ubth  29878  hcau  30189  hcaucvg  30191  hlimi  30193  hlimconvi  30196  hlim2  30197  elcnop  30862  elcnfn  30887  cnopc  30918  cnfnc  30935  lnopcon  31040  lnfncon  31061  riesz1  31070  xrge0tsmsd  31969  signsply0  33252  unblimceq0  35046  cvgcau  43846  limcleqr  44005  addlimc  44009  0ellimcdiv  44010  climd  44033  climisp  44107  lmbr3  44108  climrescn  44109  climxrrelem  44110  climxrre  44111  xlimpnfxnegmnf  44175  xlimxrre  44192  xlimmnf  44202  xlimpnf  44203  xlimmnfmpt  44204  xlimpnfmpt  44205  dfxlim2  44209  cncfshift  44235  cncfperiod  44240  ioodvbdlimc1lem1  44292  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  fourierdlem68  44535  fourierdlem87  44554  fourierdlem103  44570  fourierdlem104  44571  etransclem48  44643