Theorem example-E5.03a 665

Description: Hypothesis Elimination Example 3.

Assertion

Ref	Expression
example-E5.03a	⊢ (𝑥 = 𝑥₁ → (∀𝑧(𝑧 ∈ 𝑥 ↔ ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)) ↔ ∀𝑧(𝑧 ∈ 𝑥₁ ↔ ∀𝑎(𝑎 ∈ 𝑧 → 𝑎 ∈ 𝑦))))

Distinct variable group:   𝑥,𝑎,𝑥₁,𝑦,𝑧

Proof of Theorem example-E5.03a

Step	Hyp	Ref	Expression
1		rcp-NDASM1of1 192	. . . 4 ⊢ (𝑥 = 𝑥₁ → 𝑥 = 𝑥₁)
2	1	subelofr-P5 640	. . 3 ⊢ (𝑥 = 𝑥₁ → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥₁))
3		subelofl-P5.CL 639	. . . . . 6 ⊢ (𝑥 = 𝑎 → (𝑥 ∈ 𝑧 ↔ 𝑎 ∈ 𝑧))
4		subelofl-P5.CL 639	. . . . . 6 ⊢ (𝑥 = 𝑎 → (𝑥 ∈ 𝑦 ↔ 𝑎 ∈ 𝑦))
5	3, 4	subimd-P3.40c 329	. . . . 5 ⊢ (𝑥 = 𝑎 → ((𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦) ↔ (𝑎 ∈ 𝑧 → 𝑎 ∈ 𝑦)))
6	5	cbvallv-P5 659	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦) ↔ ∀𝑎(𝑎 ∈ 𝑧 → 𝑎 ∈ 𝑦))
7	6	rcp-NDIMP0addall 207	. . 3 ⊢ (𝑥 = 𝑥₁ → (∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦) ↔ ∀𝑎(𝑎 ∈ 𝑧 → 𝑎 ∈ 𝑦)))
8	2, 7	subbid-P3.41c 336	. 2 ⊢ (𝑥 = 𝑥₁ → ((𝑧 ∈ 𝑥 ↔ ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑥₁ ↔ ∀𝑎(𝑎 ∈ 𝑧 → 𝑎 ∈ 𝑦))))
9	8	suballv-P5 623	1 ⊢ (𝑥 = 𝑥₁ → (∀𝑧(𝑧 ∈ 𝑥 ↔ ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)) ↔ ∀𝑧(𝑧 ∈ 𝑥₁ ↔ ∀𝑎(𝑎 ∈ 𝑧 → 𝑎 ∈ 𝑦))))

Syntax hints:  term-obj 1   = wff-equals 6   ∈ wff-elemof 7  ∀wff-forall 8   → wff-imp 10   ↔ wff-bi 104

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19  ax-L8-inl 20  ax-L8-inr 21

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161  df-exists-D5.1 596

This theorem is referenced by: (None)