Theorem axsep2 2700

Description: A less restrictive version of the Separation Scheme axsep 2698, where variables x and z can both appear free in the wff φ, which can therefore be thought of as φ(x, z). This version was derived from the more restrictive ax-sep 2699 with no additional set theory axioms.

Assertion

Ref	Expression
axsep2	⊢ ∃y∀x(x ∈ y ↔ (x ∈ z ⋀ φ))

Distinct variable groups:   x,y,z   φ,y

Proof of Theorem axsep2

Step	Hyp	Ref	Expression
1		a9e 1123	. 2 ⊢ ∃w w = z
2		ax-sep 2699	. . . 4 ⊢ ∃y∀x(x ∈ y ↔ (x ∈ w ⋀ (x ∈ z ⋀ φ)))
3		elequ2 1135	. . . . . . . . . . 11 ⊢ (w = z → (x ∈ w ↔ x ∈ z))
4	3	biimprd 154	. . . . . . . . . 10 ⊢ (w = z → (x ∈ z → x ∈ w))
5	4	pm4.71rd 638	. . . . . . . . 9 ⊢ (w = z → (x ∈ z ↔ (x ∈ w ⋀ x ∈ z)))
6	5	anbi1d 616	. . . . . . . 8 ⊢ (w = z → ((x ∈ z ⋀ φ) ↔ ((x ∈ w ⋀ x ∈ z) ⋀ φ)))
7		anass 439	. . . . . . . 8 ⊢ (((x ∈ w ⋀ x ∈ z) ⋀ φ) ↔ (x ∈ w ⋀ (x ∈ z ⋀ φ)))
8	6, 7	syl6bb 535	. . . . . . 7 ⊢ (w = z → ((x ∈ z ⋀ φ) ↔ (x ∈ w ⋀ (x ∈ z ⋀ φ))))
9	8	bibi2d 617	. . . . . 6 ⊢ (w = z → ((x ∈ y ↔ (x ∈ z ⋀ φ)) ↔ (x ∈ y ↔ (x ∈ w ⋀ (x ∈ z ⋀ φ)))))
10	9	albidv 1276	. . . . 5 ⊢ (w = z → (∀x(x ∈ y ↔ (x ∈ z ⋀ φ)) ↔ ∀x(x ∈ y ↔ (x ∈ w ⋀ (x ∈ z ⋀ φ)))))
11	10	exbidv 1277	. . . 4 ⊢ (w = z → (∃y∀x(x ∈ y ↔ (x ∈ z ⋀ φ)) ↔ ∃y∀x(x ∈ y ↔ (x ∈ w ⋀ (x ∈ z ⋀ φ)))))
12	2, 11	mpbiri 194	. . 3 ⊢ (w = z → ∃y∀x(x ∈ y ↔ (x ∈ z ⋀ φ)))
13	12	19.23aiv 1293	. 2 ⊢ (∃w w = z → ∃y∀x(x ∈ y ↔ (x ∈ z ⋀ φ)))
14	1, 13	ax-mp 7	1 ⊢ ∃y∀x(x ∈ y ↔ (x ∈ z ⋀ φ))

Syntax hints:   ↔ wb 146   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-8 962  ax-9 963  ax-12 966  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-sep 2699

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979

Copyright terms: Public domain