Theorem trss 4761

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 4756	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
2		sseq1 3626	. . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
3	2	rspccv 3306	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	sylbi 207	1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 1990  ∀wral 2912   ⊆ wss 3574  Tr wtr 4752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202  df-in 3581  df-ss 3588  df-uni 4437  df-tr 4753

This theorem is referenced by:  trin  4763  triun  4766  trintss  4769  tz7.2  5098  ordelss  5739  ordelord  5745  tz7.7  5749  trsucss  5811  omsinds  7084  tc2  8618  tcel  8621  r1ord3g  8642  r1ord2  8644  r1pwss  8647  rankwflemb  8656  r1elwf  8659  r1elssi  8668  uniwf  8682  itunitc1  9242  wunelss  9530  tskr1om2  9590  tskuni  9605  tskurn  9611  gruelss  9616  dfon2lem6  31693  dfon2lem9  31696  setindtr  37591  dford3lem1  37593  ordelordALT  38747  trsspwALT  39045  trsspwALT2  39046  trsspwALT3  39047  pwtrVD  39059  ordelordALTVD  39103