Theorem bj-ax9-2 32891

Description: Proof of ax-9 1999 from Tarski's FOL=, ax-8 1992 (specifically, ax8v1 1994 and ax8v2 1995) , df-cleq 2615 and ax-ext 2602. For a version not using ax-8 1992, see bj-ax9 32890. This shows that df-cleq 2615 is "too powerful". A possible definition is given by bj-df-cleq 32893. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-ax9-2	⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))

Proof of Theorem bj-ax9-2

Dummy variables 𝑣 𝑢 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-ext 2602	. . . . 5 ⊢ (∀𝑢(𝑢 ∈ 𝑣 ↔ 𝑢 ∈ 𝑤) → 𝑣 = 𝑤)
2	1	df-cleq 2615	. . . 4 ⊢ (𝑥 = 𝑦 ↔ ∀𝑢(𝑢 ∈ 𝑥 ↔ 𝑢 ∈ 𝑦))
3	2	biimpi 206	. . 3 ⊢ (𝑥 = 𝑦 → ∀𝑢(𝑢 ∈ 𝑥 ↔ 𝑢 ∈ 𝑦))
4		biimp 205	. . 3 ⊢ ((𝑢 ∈ 𝑥 ↔ 𝑢 ∈ 𝑦) → (𝑢 ∈ 𝑥 → 𝑢 ∈ 𝑦))
5	3, 4	sylg 1750	. 2 ⊢ (𝑥 = 𝑦 → ∀𝑢(𝑢 ∈ 𝑥 → 𝑢 ∈ 𝑦))
6		ax8v2 1995	. . . . 5 ⊢ (𝑧 = 𝑢 → (𝑧 ∈ 𝑥 → 𝑢 ∈ 𝑥))
7	6	equcoms 1947	. . . 4 ⊢ (𝑢 = 𝑧 → (𝑧 ∈ 𝑥 → 𝑢 ∈ 𝑥))
8		ax8v1 1994	. . . 4 ⊢ (𝑢 = 𝑧 → (𝑢 ∈ 𝑦 → 𝑧 ∈ 𝑦))
9	7, 8	imim12d 81	. . 3 ⊢ (𝑢 = 𝑧 → ((𝑢 ∈ 𝑥 → 𝑢 ∈ 𝑦) → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)))
10	9	spimvw 1927	. 2 ⊢ (∀𝑢(𝑢 ∈ 𝑥 → 𝑢 ∈ 𝑦) → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
11	5, 10	syl 17	1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1481

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-8 1992  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by: (None)