Theorem rexralbidv 3231

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wral 3079  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080  df-rex 3090

This theorem is referenced by:  freq1  5628  rexfiuz  15395  cau3lem  15402  caubnd2  15405  climi  15557  rlimi  15560  o1lo1  15584  2clim  15619  lo1le  15699  caucvgrlem  15720  caurcvgr  15721  caucvgb  15727  vdwlem10  17045  vdwlem13  17048  pmatcollpw2lem  22934  neiptopnei  23289  lmcvg  23419  lmss  23455  elpt  23729  elptr  23730  txlm  23805  tsmsi  24291  ustuqtop4  24401  isucn  24434  isucn2  24435  ucnima  24437  metcnpi  24701  metcnpi2  24702  metucn  24728  xrge0tsms  24992  elcncf  25048  cncfi  25053  lmmcvg  25420  lhop1  26173  ulmval  26543  ulmi  26549  ulmcaulem  26557  ulmdvlem3  26565  pntibnd  27757  pntlem3  27773  pntleml  27775  axtgcont1  28737  perpln1  28990  perpln2  28991  isperp  28992  brbtwn  29249  uvtx01vtx  29747  isgrpo  30849  ubthlem3  31224  ubth  31225  hcau  31536  hcaucvg  31538  hlimi  31540  hlimconvi  31543  hlim2  31544  elcnop  32209  elcnfn  32234  cnopc  32265  cnfnc  32282  lnopcon  32387  lnfncon  32408  riesz1  32417  xrge0tsmsd  33393  signsply0  34938  unblimceq0  37116  cvgcau  46224  limcleqr  46378  addlimc  46382  0ellimcdiv  46383  climd  46406  climisp  46480  lmbr3  46481  climrescn  46482  climxrrelem  46483  climxrre  46484  xlimpnfxnegmnf  46548  xlimxrre  46565  xlimmnf  46575  xlimpnf  46576  xlimmnfmpt  46577  xlimpnfmpt  46578  dfxlim2  46582  cncfshift  46608  cncfperiod  46613  ioodvbdlimc1lem1  46665  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  fourierdlem68  46908  fourierdlem87  46927  fourierdlem103  46943  fourierdlem104  46944  etransclem48  47016