Theorem abssi 4067

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 4063	. 2 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝑥 ∈ 𝐴}
3		abid2 2872	. 2 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴
4	2, 3	sseqtri 4018	1 ⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴

Syntax hints:   → wi 4   ∈ wcel 2107  {cab 2710   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  ssab2  4076  intab  4982  opabss  5212  relopabiALT  5822  exse2  7905  opiota  8042  mpoexw  8062  fsplitfpar  8101  tfrlem8  8381  fiprc  9042  fival  9404  hartogslem1  9534  dmttrcl  9713  rnttrcl  9714  tz9.12lem1  9779  rankuni  9855  scott0  9878  r0weon  10004  alephval3  10102  aceq3lem  10112  dfac5lem4  10118  dfac2b  10122  cff  10240  cfsuc  10249  cff1  10250  cflim2  10255  cfss  10257  axdc3lem  10442  axdclem  10511  gruina  10810  nqpr  11006  infcvgaux1i  15800  4sqlem1  16878  sscpwex  17759  cssval  21227  topnex  22491  islocfin  23013  hauspwpwf1  23483  itg2lcl  25237  2sqlem7  26917  scutf  27303  isismt  27775  nmcexi  31267  opabssi  31830  lsmsnorb  32490  dispcmp  32828  cnre2csqima  32880  mppspstlem  34551  colinearex  35021  itg2addnclem  36528  itg2addnc  36531  eldiophb  41481