Theorem rexralbidv 3219

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 3176	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3177	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 1796  ax-4 1810  ax-5 1912

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

This theorem is referenced by:  freq1  5647  rexfiuz  15299  cau3lem  15306  caubnd2  15309  climi  15459  rlimi  15462  o1lo1  15486  2clim  15521  lo1le  15603  caucvgrlem  15624  caurcvgr  15625  caucvgb  15631  vdwlem10  16928  vdwlem13  16931  pmatcollpw2lem  22500  neiptopnei  22857  lmcvg  22987  lmss  23023  elpt  23297  elptr  23298  txlm  23373  tsmsi  23859  ustuqtop4  23970  isucn  24004  isucn2  24005  ucnima  24007  metcnpi  24274  metcnpi2  24275  metucn  24301  xrge0tsms  24571  elcncf  24630  cncfi  24635  lmmcvg  25010  lhop1  25764  ulmval  26125  ulmi  26131  ulmcaulem  26139  ulmdvlem3  26147  pntibnd  27329  pntlem3  27345  pntleml  27347  axtgcont1  27983  perpln1  28225  perpln2  28226  isperp  28227  brbtwn  28421  uvtx01vtx  28918  isgrpo  30014  ubthlem3  30389  ubth  30390  hcau  30701  hcaucvg  30703  hlimi  30705  hlimconvi  30708  hlim2  30709  elcnop  31374  elcnfn  31399  cnopc  31430  cnfnc  31447  lnopcon  31552  lnfncon  31573  riesz1  31582  xrge0tsmsd  32476  signsply0  33857  unblimceq0  35687  cvgcau  44501  limcleqr  44660  addlimc  44664  0ellimcdiv  44665  climd  44688  climisp  44762  lmbr3  44763  climrescn  44764  climxrrelem  44765  climxrre  44766  xlimpnfxnegmnf  44830  xlimxrre  44847  xlimmnf  44857  xlimpnf  44858  xlimmnfmpt  44859  xlimpnfmpt  44860  dfxlim2  44864  cncfshift  44890  cncfperiod  44895  ioodvbdlimc1lem1  44947  ioodvbdlimc1lem2  44948  ioodvbdlimc2lem  44950  fourierdlem68  45190  fourierdlem87  45209  fourierdlem103  45225  fourierdlem104  45226  etransclem48  45298