Theorem r19.21bi 2558

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

Syntax hints:   → wi 4   ∧ wa 103  ∀wal 1346   ∈ wcel 2141  ∀wral 2448

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

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

This theorem is referenced by:  rspec2  2559  rspec3  2560  r19.21be  2561  frind  4337  wepo  4344  wetrep  4345  ordelord  4366  ralxfr2d  4449  rexxfr2d  4450  funfveu  5509  fvmptelrn  5649  f1oresrab  5661  isoselem  5799  mpoexw  6192  disjxp1  6215  tfrlemisucaccv  6304  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  xpf1o  6822  fimax2gtrilemstep  6878  supisoti  6987  difinfsn  7077  exmidomni  7118  cc3  7230  prcdnql  7446  prcunqu  7447  prdisj  7454  caucvgsrlembound  7756  caucvgsrlemoffgt1  7761  exbtwnzlemex  10206  monoord2  10433  iseqf1olemqk  10450  seq3f1olemqsumk  10455  caucvgrelemcau  10944  fimaxre2  11190  climrecvg1n  11311  zsumdc  11347  fsum3  11350  isumss2  11356  fsum3ser  11360  sumpr  11376  sumtp  11377  fsum2dlemstep  11397  fsumiun  11440  isumlessdc  11459  zproddc  11542  fprodsplitdc  11559  fprodcl2lem  11568  fprod2dlemstep  11585  bezoutlemstep  11952  ennnfonelemim  12379  ctiunctal  12396  grppropd  12724  cnmpt11  13077  psmet0  13121  psmettri2  13122  mulcncflem  13384  mulcncf  13385  dedekindeulemuub  13389  dedekindeulemlu  13393  dedekindicclemuub  13398  dedekindicclemlu  13402  limccnpcntop  13438  limccnp2lem  13439  limccnp2cntop  13440  bj-charfundc  13843  bj-charfunbi  13846  nninffeq  14053  refeq  14060  iswomni0  14083  nconstwlpolem  14096