Theorem r19.21bi 2523

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 2422	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	sylib 121	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4	3	19.21bi 1538	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
5	4	imp 123	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103  ∀wal 1330   ∈ wcel 1481  ∀wral 2417

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

This theorem depends on definitions:  df-bi 116  df-ral 2422

This theorem is referenced by:  rspec2  2524  rspec3  2525  r19.21be  2526  frind  4282  wepo  4289  wetrep  4290  ordelord  4311  ralxfr2d  4393  rexxfr2d  4394  funfveu  5442  fvmptelrn  5581  f1oresrab  5593  isoselem  5729  disjxp1  6141  tfrlemisucaccv  6230  tfr1onlemsucaccv  6246  tfrcllemsucaccv  6259  xpf1o  6746  fimax2gtrilemstep  6802  supisoti  6905  difinfsn  6993  exmidomni  7022  cc3  7100  prcdnql  7316  prcunqu  7317  prdisj  7324  caucvgsrlembound  7626  caucvgsrlemoffgt1  7631  exbtwnzlemex  10058  monoord2  10281  iseqf1olemqk  10298  seq3f1olemqsumk  10303  caucvgrelemcau  10784  fimaxre2  11030  climrecvg1n  11149  zsumdc  11185  fsum3  11188  isumss2  11194  fsum3ser  11198  sumpr  11214  sumtp  11215  fsum2dlemstep  11235  fsumiun  11278  isumlessdc  11297  zproddc  11380  bezoutlemstep  11721  ennnfonelemim  11973  ctiunctal  11990  cnmpt11  12491  psmet0  12535  psmettri2  12536  mulcncflem  12798  mulcncf  12799  dedekindeulemuub  12803  dedekindeulemlu  12807  dedekindicclemuub  12812  dedekindicclemlu  12816  limccnpcntop  12852  limccnp2lem  12853  limccnp2cntop  12854  nninffeq  13391  refeq  13398