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 3574	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	sylbi 220	1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3077   ⊆ 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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-v 3453  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  5634  trpred  6333  ordelss  6377  ordelord  6383  tz7.7  6387  trsucss  6452  tc2  9734  tcel  9737  r1ord3g  9779  r1ord2  9781  r1pwss  9784  rankwflemb  9793  rankwflembOLD  9794  r1elwf  9797  r1elssi  9806  uniwf  9821  itunitc1  10491  wunelss  10786  tskhf  10846  tskuni  10861  tskurn  10867  gruelss  10872  tz9.1regs  35785  dfon2lem6  36530  dfon2lem9  36533  nmuladdss  36942  axtco2g  37245  tr0elw  37252  tr0el  37253  ttctr2  37262  ttciunun  37279  setindtr  44010  dford3lem1  44012  ordelordALT  45505  trsspwALT  45785  trsspwALT2  45786  trsspwALT3  45787  pwtrVD  45791  ordelordALTVD  45834  ralabso  45936  rexabso  45937  modelaxrep  45949  omelaxinf2  45957