Theorem rexralbidv 3203

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3044  ∃wrex 3053

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 3045  df-rex 3054

This theorem is referenced by:  freq1  5605  rexfiuz  15314  cau3lem  15321  caubnd2  15324  climi  15476  rlimi  15479  o1lo1  15503  2clim  15538  lo1le  15618  caucvgrlem  15639  caurcvgr  15640  caucvgb  15646  vdwlem10  16961  vdwlem13  16964  pmatcollpw2lem  22664  neiptopnei  23019  lmcvg  23149  lmss  23185  elpt  23459  elptr  23460  txlm  23535  tsmsi  24021  ustuqtop4  24132  isucn  24165  isucn2  24166  ucnima  24168  metcnpi  24432  metcnpi2  24433  metucn  24459  xrge0tsms  24723  elcncf  24782  cncfi  24787  lmmcvg  25161  lhop1  25919  ulmval  26289  ulmi  26295  ulmcaulem  26303  ulmdvlem3  26311  pntibnd  27504  pntlem3  27520  pntleml  27522  axtgcont1  28395  perpln1  28637  perpln2  28638  isperp  28639  brbtwn  28826  uvtx01vtx  29324  isgrpo  30426  ubthlem3  30801  ubth  30802  hcau  31113  hcaucvg  31115  hlimi  31117  hlimconvi  31120  hlim2  31121  elcnop  31786  elcnfn  31811  cnopc  31842  cnfnc  31859  lnopcon  31964  lnfncon  31985  riesz1  31994  xrge0tsmsd  33002  signsply0  34542  unblimceq0  36495  cvgcau  45486  limcleqr  45642  addlimc  45646  0ellimcdiv  45647  climd  45670  climisp  45744  lmbr3  45745  climrescn  45746  climxrrelem  45747  climxrre  45748  xlimpnfxnegmnf  45812  xlimxrre  45829  xlimmnf  45839  xlimpnf  45840  xlimmnfmpt  45841  xlimpnfmpt  45842  dfxlim2  45846  cncfshift  45872  cncfperiod  45877  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  fourierdlem68  46172  fourierdlem87  46191  fourierdlem103  46207  fourierdlem104  46208  etransclem48  46280