Theorem trss 5222

Description: An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.) (Proof shortened by JJ, 26-Jul-2021.)

Assertion

Ref	Expression
trss	⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Proof of Theorem trss

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dftr3 5217	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
2		sseq1 3956	. . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
3	2	rspccv 3573	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	sylbi 220	1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3076   ⊆ wss 3899  Tr wtr 5212

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3916  df-uni 4868  df-tr 5213

This theorem is used by:  trun  5223  trin  5224  triun  5227  triin  5229  trintss  5231  tz7.2  5638  trpred  6329  ordelss  6373  ordelord  6379  tz7.7  6383  trsucss  6448  tc2  9719  tcel  9722  r1ord3g  9761  r1ord2  9763  r1pwss  9766  rankwflemb  9775  r1elwf  9778  r1elssi  9787  uniwf  9801  itunitc1  10422  wunelss  10717  tskr1om2  10777  tskuni  10792  tskurn  10798  gruelss  10803  tz9.1regs  35660  dfon2lem6  36365  dfon2lem9  36368  nmuladdss  36793  axtco2g  37096  tr0elw  37103  tr0el  37104  ttctr2  37113  ttciunun  37130  setindtr  43865  dford3lem1  43867  ordelordALT  45360  trsspwALT  45640  trsspwALT2  45641  trsspwALT3  45642  pwtrVD  45646  ordelordALTVD  45689  ralabso  45791  rexabso  45792  modelaxrep  45804  omelaxinf2  45812