Theorem abssi 4033

Description: Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)

Hypothesis

Ref	Expression
abssi.1	⊢ (𝜑 → 𝑥 ∈ 𝐴)

Assertion

Ref	Expression
abssi	⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem abssi

Step	Hyp	Ref	Expression
1		abssi.1	. . 3 ⊢ (𝜑 → 𝑥 ∈ 𝐴)
2	1	ss2abi 4030	. 2 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝑥 ∈ 𝐴}
3		abid2 2865	. 2 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴
4	2, 3	sseqtri 3995	1 ⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴

Syntax hints:   → wi 4   ∈ wcel 2109  {cab 2707   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931

This theorem is referenced by:  ssab2  4042  intab  4942  opabss  5171  relopabiALT  5786  exse2  7893  opiota  8038  mpoexw  8057  fsplitfpar  8097  tfrlem8  8352  fiprc  9016  fival  9363  hartogslem1  9495  dmttrcl  9674  rnttrcl  9675  tz9.12lem1  9740  rankuni  9816  scott0  9839  r0weon  9965  alephval3  10063  aceq3lem  10073  dfac5lem4  10079  dfac5lem4OLD  10081  dfac2b  10084  cff  10201  cfsuc  10210  cff1  10211  cflim2  10216  cfss  10218  axdc3lem  10403  axdclem  10472  gruina  10771  nqpr  10967  infcvgaux1i  15823  4sqlem1  16919  sscpwex  17777  cssval  21591  topnex  22883  islocfin  23404  hauspwpwf1  23874  itg2lcl  25628  2sqlem7  27335  scutf  27724  isismt  28461  nmcexi  31955  opabssi  32541  lsmsnorb  33362  dispcmp  33849  cnre2csqima  33901  mppspstlem  35558  colinearex  36048  itg2addnclem  37665  itg2addnc  37668  eldiophb  42745