Theorem abssi 4065

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

Syntax hints:   → wi 4   ∈ wcel 2098  {cab 2704   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3473  df-in 3954  df-ss 3964

This theorem is referenced by:  ssab2  4074  intab  4983  opabss  5214  relopabiALT  5827  exse2  7929  opiota  8067  mpoexw  8087  fsplitfpar  8127  tfrlem8  8409  fiprc  9074  fival  9441  hartogslem1  9571  dmttrcl  9750  rnttrcl  9751  tz9.12lem1  9816  rankuni  9892  scott0  9915  r0weon  10041  alephval3  10139  aceq3lem  10149  dfac5lem4  10155  dfac2b  10159  cff  10277  cfsuc  10286  cff1  10287  cflim2  10292  cfss  10294  axdc3lem  10479  axdclem  10548  gruina  10847  nqpr  11043  infcvgaux1i  15841  4sqlem1  16922  sscpwex  17803  cssval  21619  topnex  22917  islocfin  23439  hauspwpwf1  23909  itg2lcl  25675  2sqlem7  27375  scutf  27763  isismt  28356  nmcexi  31854  opabssi  32421  lsmsnorb  33118  dispcmp  33465  cnre2csqima  33517  mppspstlem  35186  colinearex  35661  itg2addnclem  37149  itg2addnc  37152  eldiophb  42180

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »