Theorem dftr2 5202

Description: An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. Using dftr2c 5203 instead may avoid dependences on ax-11 2160. (Contributed by NM, 24-Apr-1994.)

Assertion

Ref	Expression
dftr2	⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))

Distinct variable group:   𝑥,𝑦,𝐴

Proof of Theorem dftr2

Step	Hyp	Ref	Expression
1		df-ss 3914	. 2 ⊢ (∪ 𝐴 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴))
2		df-tr 5201	. 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
3		19.23v 1943	. . . 4 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
4		eluni 4861	. . . . 5 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5	4	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
6	3, 5	bitr4i 278	. . 3 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴))
7	6	albii 1820	. 2 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ ∀𝑥(𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴))
8	1, 2, 7	3bitr4i 303	1 ⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539  ∃wex 1780   ∈ wcel 2111   ⊆ wss 3897  ∪ cuni 4858  Tr wtr 5200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4859  df-tr 5201

This theorem is referenced by:  dftr2c  5203  trel  5208  ordelord  6334  suctr  6400  trom  7811  hartogs  9436  card2on  9446  trcl  9624  tskwe  9849  ondomon  10460  nosupno  27648  noinfno  27663  bdayon  28215  dftr6  35802  elpotr  35830  hftr  36233  dford4  43127  mnutrd  44378  tratrb  44634  trsbc  44638  truniALT  44639  sspwtr  44918  sspwtrALT  44919  sspwtrALT2  44920  pwtrVD  44921  pwtrrVD  44922  suctrALT  44923  suctrALT2VD  44933  suctrALT2  44934  tratrbVD  44958  trsbcVD  44974  truniALTVD  44975  trintALTVD  44977  trintALT  44978  suctrALTcf  45019  suctrALTcfVD  45020  suctrALT3  45021