Theorem dftr2 5218

Description: An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. Using dftr2c 5219 instead may avoid dependences on ax-11 2197. (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 3901	. 2 ⊢ (∪ 𝐴 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴))
2		df-tr 5217	. 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
3		19.23v 1977	. . . 4 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
4		eluni 4873	. . . . 5 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5	4	imbi1i 352	. . . 4 ⊢ ((𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
6	3, 5	bitr4i 281	. . 3 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴))
7	6	albii 1852	. 2 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ ∀𝑥(𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴))
8	1, 2, 7	3bitr4i 306	1 ⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃wex 1812   ∈ wcel 2147   ⊆ wss 3900  ∪ cuni 4870  Tr wtr 5216

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871  df-tr 5217

This theorem is used by:  dftr2c  5219  trel  5224  ordelord  6405  suctr  6472  trom  7913  hartogs  9568  card2on  9578  trcl  9759  tskwe  10061  ondomon  10677  nosupno  28093  noinfno  28108  bdayons  28695  dftr6  36707  elpotr  36734  hftr  37124  ttctr  37472  dfttc2g  37485  dfttc4lem2  37508  dford4  44240  mnutrd  45467  tratrb  45721  trsbc  45725  truniALT  45726  sspwtr  46005  sspwtrALT  46006  sspwtrALT2  46007  pwtrVD  46008  pwtrrVD  46009  suctrALT  46010  suctrALT2VD  46020  suctrALT2  46021  tratrbVD  46045  trsbcVD  46061  truniALTVD  46062  trintALTVD  46064  trintALT  46065  suctrALTcf  46106  suctrALTcfVD  46107  suctrALT3  46108