Theorem dftr2 5195

Description: An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. Using dftr2c 5196 instead may avoid dependences on ax-11 2163. (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 3907	. 2 ⊢ (∪ 𝐴 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴))
2		df-tr 5194	. 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
3		19.23v 1944	. . . 4 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
4		eluni 4854	. . . . 5 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5	4	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
6	3, 5	bitr4i 278	. . 3 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴))
7	6	albii 1821	. 2 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ ∀𝑥(𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴))
8	1, 2, 7	3bitr4i 303	1 ⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540  ∃wex 1781   ∈ wcel 2114   ⊆ wss 3890  ∪ cuni 4851  Tr wtr 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852  df-tr 5194

This theorem is referenced by:  dftr2c  5196  trel  5201  ordelord  6339  suctr  6405  trom  7819  hartogs  9452  card2on  9462  trcl  9640  tskwe  9865  ondomon  10476  nosupno  27681  noinfno  27696  bdayons  28282  dftr6  35949  elpotr  35977  hftr  36380  ttctr  36691  dfttc2g  36704  dfttc4lem2  36727  dford4  43475  mnutrd  44725  tratrb  44981  trsbc  44985  truniALT  44986  sspwtr  45265  sspwtrALT  45266  sspwtrALT2  45267  pwtrVD  45268  pwtrrVD  45269  suctrALT  45270  suctrALT2VD  45280  suctrALT2  45281  tratrbVD  45305  trsbcVD  45321  truniALTVD  45322  trintALTVD  45324  trintALT  45325  suctrALTcf  45366  suctrALTcfVD  45367  suctrALT3  45368