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  4497  wepo  4504  wetrep  4505  ordelord  4526  ralxfr2d  4610  rexxfr2d  4611  funfveu  5708  fvmptelcdm  5861  f1oresrab  5873  isoselem  6026  mpoexw  6449  disjxp1  6472  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  xpf1o  7144  fimax2gtrilemstep  7205  supisoti  7350  difinfsn  7440  exmidomni  7482  cc3  7634  prcdnql  7851  prcunqu  7852  prdisj  7859  caucvgsrlembound  8161  caucvgsrlemoffgt1  8166  exbtwnzlemex  10694  monoord2  10936  iseqf1olemqk  10957  seq3f1olemqsumk  10962  caucvgrelemcau  11760  fimaxre2  12008  climrecvg1n  12130  zsumdc  12167  fsum3  12170  isumss2  12176  fsum3ser  12180  sumpr  12196  sumtp  12197  fsum2dlemstep  12217  fsumiun  12260  isumlessdc  12279  zproddc  12362  fprodsplitdc  12379  fprodcl2lem  12388  fprod2dlemstep  12405  bezoutlemstep  12790  ennnfonelemim  13364  ctiunctal  13381  grppropd  13871  prdsmndd  14243  srgdilem  14322  srgrz  14337  srglz  14338  psrbagcon  15111  cnmpt11  15433  psmet0  15477  psmettri2  15478  mulcncflem  15757  mulcncf  15758  dedekindeulemuub  15767  dedekindeulemlu  15771  dedekindicclemuub  15776  dedekindicclemlu  15780  limccnpcntop  15825  limccnp2lem  15826  limccnp2cntop  15827  plycoeid3  15907  fsumdvdsmul  16186  bj-charfundc  16932  bj-charfunbi  16935  nninffeq  17161  refeq  17171  iswomni0  17199  nconstwlpolem  17213