Theorem rexralbidv 3229

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wral 3077  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3078  df-rex 3088

This theorem is used by:  freq1  5618  rexfiuz  15515  cau3lem  15522  caubnd2  15525  climi  15677  rlimi  15680  o1lo1  15704  2clim  15739  lo1le  15819  caucvgrlem  15840  caurcvgr  15841  caucvgb  15847  vdwlem10  17168  vdwlem13  17171  pmatcollpw2lem  23095  neiptopnei  23450  lmcvg  23580  lmss  23616  elpt  23891  elptr  23892  txlm  23967  tsmsi  24453  ustuqtop4  24563  isucn  24596  isucn2  24597  ucnima  24599  metcnpi  24863  metcnpi2  24864  metucn  24890  xrge0tsms  25154  elcncf  25210  cncfi  25215  lmmcvg  25582  lhop1  26334  ulmval  26707  ulmi  26713  ulmcaulem  26721  ulmdvlem3  26729  pntibnd  27920  pntlem3  27936  pntleml  27938  axtgcont1  28930  perpln1  29185  perpln2  29186  isperp  29187  brbtwn  29477  uvtx01vtx  29978  isgrpo  31099  ubthlem3  31474  ubth  31475  hcau  31786  hcaucvg  31788  hlimi  31790  hlimconvi  31793  hlim2  31794  elcnop  32459  elcnfn  32484  cnopc  32515  cnfnc  32532  lnopcon  32637  lnfncon  32658  riesz1  32667  xrge0tsmsd  33634  signsply0  35180  unblimceq0  37373  cvgcau  46499  limcleqr  46653  addlimc  46657  0ellimcdiv  46658  climd  46681  climisp  46755  lmbr3  46756  climrescn  46757  climxrrelem  46758  climxrre  46759  xlimpnfxnegmnf  46823  xlimxrre  46840  xlimmnf  46850  xlimpnf  46851  xlimmnfmpt  46852  xlimpnfmpt  46853  dfxlim2  46857  cncfshift  46883  cncfperiod  46888  ioodvbdlimc1lem1  46940  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  fourierdlem68  47183  fourierdlem87  47202  fourierdlem103  47218  fourierdlem104  47219  etransclem48  47291