Theorem r19.21bi 2638

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104  ∀wal 1400   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-4 1563

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  rspec2  2639  rspec3  2640  r19.21be  2641  frind  4499  wepo  4506  wetrep  4507  ordelord  4528  ralxfr2d  4612  rexxfr2d  4613  funfveu  5711  fvmptelcdm  5864  f1oresrab  5876  isoselem  6029  mpoexw  6453  disjxp1  6476  tfrlemisucaccv  6600  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  xpf1o  7148  fimax2gtrilemstep  7209  supisoti  7356  difinfsn  7446  exmidomni  7488  cc3  7640  prcdnql  7857  prcunqu  7858  prdisj  7865  caucvgsrlembound  8167  caucvgsrlemoffgt1  8172  exbtwnzlemex  10701  monoord2  10944  iseqf1olemqk  10965  seq3f1olemqsumk  10970  caucvgrelemcau  11768  fimaxre2  12016  climrecvg1n  12139  zsumdc  12176  fsum3  12179  isumss2  12185  fsum3ser  12189  sumpr  12205  sumtp  12206  fsum2dlemstep  12226  fsumiun  12269  isumlessdc  12288  zproddc  12371  fprodsplitdc  12388  fprodcl2lem  12397  fprod2dlemstep  12414  bezoutlemstep  12799  ennnfonelemim  13373  ctiunctal  13390  grppropd  13881  gsummptfidmsplit  14254  prdsmndd  14301  srgdilem  14380  srgrz  14395  srglz  14396  psrbagcon  15171  cnmpt11  15509  psmet0  15553  psmettri2  15554  mulcncflem  15833  mulcncf  15834  dedekindeulemuub  15843  dedekindeulemlu  15847  dedekindicclemuub  15852  dedekindicclemlu  15856  limccnpcntop  15901  limccnp2lem  15902  limccnp2cntop  15903  plycoeid3  15983  fsumdvdsmul  16285  bj-charfundc  17039  bj-charfunbi  17042  nninffeq  17269  refeq  17279  iswomni0  17308  nconstwlpolem  17322