Theorem r19.21bi 2618

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 2513	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	sylib 122	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4	3	19.21bi 1604	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
5	4	imp 124	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1393   ∈ wcel 2200  ∀wral 2508

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

This theorem depends on definitions:  df-bi 117  df-ral 2513

This theorem is referenced by:  rspec2  2619  rspec3  2620  r19.21be  2621  frind  4442  wepo  4449  wetrep  4450  ordelord  4471  ralxfr2d  4554  rexxfr2d  4555  funfveu  5639  fvmptelcdm  5787  f1oresrab  5799  isoselem  5943  mpoexw  6357  disjxp1  6380  tfrlemisucaccv  6469  tfr1onlemsucaccv  6485  tfrcllemsucaccv  6498  xpf1o  7001  fimax2gtrilemstep  7058  supisoti  7173  difinfsn  7263  exmidomni  7305  cc3  7450  prcdnql  7667  prcunqu  7668  prdisj  7675  caucvgsrlembound  7977  caucvgsrlemoffgt1  7982  exbtwnzlemex  10464  monoord2  10703  iseqf1olemqk  10724  seq3f1olemqsumk  10729  caucvgrelemcau  11486  fimaxre2  11733  climrecvg1n  11854  zsumdc  11890  fsum3  11893  isumss2  11899  fsum3ser  11903  sumpr  11919  sumtp  11920  fsum2dlemstep  11940  fsumiun  11983  isumlessdc  12002  zproddc  12085  fprodsplitdc  12102  fprodcl2lem  12111  fprod2dlemstep  12128  bezoutlemstep  12513  ennnfonelemim  12990  ctiunctal  13007  prdsmndd  13476  grppropd  13545  srgdilem  13927  srgrz  13942  srglz  13943  cnmpt11  14951  psmet0  14995  psmettri2  14996  mulcncflem  15275  mulcncf  15276  dedekindeulemuub  15285  dedekindeulemlu  15289  dedekindicclemuub  15294  dedekindicclemlu  15298  limccnpcntop  15343  limccnp2lem  15344  limccnp2cntop  15345  plycoeid3  15425  fsumdvdsmul  15659  bj-charfundc  16129  bj-charfunbi  16132  nninffeq  16345  refeq  16355  iswomni0  16378  nconstwlpolem  16392