ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ssexd GIF version

Theorem ssexd 4169
Description: A subclass of a set is a set. Deduction form of ssexg 4168. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
ssexd.1 (𝜑𝐵𝐶)
ssexd.2 (𝜑𝐴𝐵)
Assertion
Ref Expression
ssexd (𝜑𝐴 ∈ V)

Proof of Theorem ssexd
StepHypRef Expression
1 ssexd.2 . 2 (𝜑𝐴𝐵)
2 ssexd.1 . 2 (𝜑𝐵𝐶)
3 ssexg 4168 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
41, 2, 3syl2anc 411 1 (𝜑𝐴 ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2164  Vcvv 2760  wss 3153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4147
This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-in 3159  df-ss 3166
This theorem is referenced by:  iotaexab  5233  fex2  5422  riotaexg  5877  opabbrex  5962  funexw  6164  f1imaen2g  6847  pw2f1odclem  6890  fiss  7036  genipv  7569  suplocexprlemlub  7784  hashfacen  10907  ovshftex  10963  strslssd  12665  ressbas2d  12686  ressval3d  12690  ressabsg  12694  restid2  12859  ptex  12875  divsfval  12911  divsfvalg  12912  igsumvalx  12972  issubmnd  13023  ress0g  13024  issubg2m  13259  releqgg  13290  eqgex  13291  eqgfval  13292  isghm  13313  ringidss  13525  reldvdsrsrg  13588  dvdsrvald  13589  dvdsrex  13594  unitgrp  13612  unitabl  13613  unitlinv  13622  unitrinv  13623  dvrfvald  13629  rdivmuldivd  13640  invrpropdg  13645  rhmunitinv  13674  subrgugrp  13736  aprval  13778  aprap  13782  sralemg  13934  srascag  13938  sravscag  13939  sraipg  13940  sraex  13942  2basgeng  14250  cnrest2  14404  cnptopresti  14406  cnptoprest  14407  cnptoprest2  14408  cnmpt2res  14465  psmetres2  14501  xmetres2  14547  limccnp2lem  14830  limccnp2cntop  14831  dvfvalap  14835  dvmulxxbr  14851  dvaddxx  14852  dvmulxx  14853  dviaddf  14854  dvimulf  14855  dvcoapbr  14856  dvmptaddx  14866  dvmptmulx  14867
  Copyright terms: Public domain W3C validator