Theorem r19.21bi 2461

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
r19.21bi.1	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Assertion

Ref	Expression
r19.21bi	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Proof of Theorem r19.21bi

Step	Hyp	Ref	Expression
1		r19.21bi.1	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
2		df-ral 2364	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	sylib 120	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4	3	19.21bi 1495	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
5	4	imp 122	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 102  ∀wal 1287   ∈ wcel 1438  ∀wral 2359

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-4 1445

This theorem depends on definitions:  df-bi 115  df-ral 2364

This theorem is referenced by:  rspec2  2462  rspec3  2463  r19.21be  2464  frind  4179  wepo  4186  wetrep  4187  ordelord  4208  ralxfr2d  4286  rexxfr2d  4287  funfveu  5318  f1oresrab  5463  isoselem  5599  disjxp1  6001  tfrlemisucaccv  6090  tfr1onlemsucaccv  6106  tfrcllemsucaccv  6119  xpf1o  6560  fimax2gtrilemstep  6616  supisoti  6705  exmidomni  6798  prcdnql  7043  prcunqu  7044  prdisj  7051  caucvgsrlembound  7339  caucvgsrlemoffgt1  7344  exbtwnzlemex  9661  monoord2  9905  iseqf1olemqk  9923  seq3f1olemqsumk  9928  caucvgrelemcau  10413  fimaxre2  10658  climrecvg1n  10737  zisum  10774  fisum  10778  isumss2  10785  fisumser  10790  sumpr  10807  sumtp  10808  fsum2dlemstep  10828  fsumiun  10871  isumlessdc  10890  bezoutlemstep  11264