Theorem dftr2 5207

Description: An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. Using dftr2c 5208 instead may avoid dependences on ax-11 2162. (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 3918	. 2 ⊢ (∪ 𝐴 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴))
2		df-tr 5206	. 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
3		19.23v 1943	. . . 4 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
4		eluni 4866	. . . . 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 2113   ⊆ wss 3901  ∪ cuni 4863  Tr wtr 5205

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-uni 4864  df-tr 5206

This theorem is referenced by:  dftr2c  5208  trel  5213  ordelord  6339  suctr  6405  trom  7817  hartogs  9449  card2on  9459  trcl  9637  tskwe  9862  ondomon  10473  nosupno  27671  noinfno  27686  bdayons  28272  dftr6  35945  elpotr  35973  hftr  36376  dford4  43267  mnutrd  44517  tratrb  44773  trsbc  44777  truniALT  44778  sspwtr  45057  sspwtrALT  45058  sspwtrALT2  45059  pwtrVD  45060  pwtrrVD  45061  suctrALT  45062  suctrALT2VD  45072  suctrALT2  45073  tratrbVD  45097  trsbcVD  45113  truniALTVD  45114  trintALTVD  45116  trintALT  45117  suctrALTcf  45158  suctrALTcfVD  45159  suctrALT3  45160