Theorem rexralbidv 3204

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 3045  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3046  df-rex 3055

This theorem is referenced by:  freq1  5608  rexfiuz  15321  cau3lem  15328  caubnd2  15331  climi  15483  rlimi  15486  o1lo1  15510  2clim  15545  lo1le  15625  caucvgrlem  15646  caurcvgr  15647  caucvgb  15653  vdwlem10  16968  vdwlem13  16971  pmatcollpw2lem  22671  neiptopnei  23026  lmcvg  23156  lmss  23192  elpt  23466  elptr  23467  txlm  23542  tsmsi  24028  ustuqtop4  24139  isucn  24172  isucn2  24173  ucnima  24175  metcnpi  24439  metcnpi2  24440  metucn  24466  xrge0tsms  24730  elcncf  24789  cncfi  24794  lmmcvg  25168  lhop1  25926  ulmval  26296  ulmi  26302  ulmcaulem  26310  ulmdvlem3  26318  pntibnd  27511  pntlem3  27527  pntleml  27529  axtgcont1  28402  perpln1  28644  perpln2  28645  isperp  28646  brbtwn  28833  uvtx01vtx  29331  isgrpo  30433  ubthlem3  30808  ubth  30809  hcau  31120  hcaucvg  31122  hlimi  31124  hlimconvi  31127  hlim2  31128  elcnop  31793  elcnfn  31818  cnopc  31849  cnfnc  31866  lnopcon  31971  lnfncon  31992  riesz1  32001  xrge0tsmsd  33009  signsply0  34549  unblimceq0  36502  cvgcau  45493  limcleqr  45649  addlimc  45653  0ellimcdiv  45654  climd  45677  climisp  45751  lmbr3  45752  climrescn  45753  climxrrelem  45754  climxrre  45755  xlimpnfxnegmnf  45819  xlimxrre  45836  xlimmnf  45846  xlimpnf  45847  xlimmnfmpt  45848  xlimpnfmpt  45849  dfxlim2  45853  cncfshift  45879  cncfperiod  45884  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  fourierdlem68  46179  fourierdlem87  46198  fourierdlem103  46214  fourierdlem104  46215  etransclem48  46287