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  10684  monoord2  10923  iseqf1olemqk  10944  seq3f1olemqsumk  10949  caucvgrelemcau  11746  fimaxre2  11993  climrecvg1n  12114  zsumdc  12151  fsum3  12154  isumss2  12160  fsum3ser  12164  sumpr  12180  sumtp  12181  fsum2dlemstep  12201  fsumiun  12244  isumlessdc  12263  zproddc  12346  fprodsplitdc  12363  fprodcl2lem  12372  fprod2dlemstep  12389  bezoutlemstep  12774  ennnfonelemim  13315  ctiunctal  13332  grppropd  13822  prdsmndd  14194  srgdilem  14273  srgrz  14288  srglz  14289  psrbagcon  15062  cnmpt11  15384  psmet0  15428  psmettri2  15429  mulcncflem  15708  mulcncf  15709  dedekindeulemuub  15718  dedekindeulemlu  15722  dedekindicclemuub  15727  dedekindicclemlu  15731  limccnpcntop  15776  limccnp2lem  15777  limccnp2cntop  15778  plycoeid3  15858  fsumdvdsmul  16105  bj-charfundc  16834  bj-charfunbi  16837  nninffeq  17063  refeq  17073  iswomni0  17101  nconstwlpolem  17115