Theorem bnj89

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bnj89.1	⊢ 𝑍 ∈ V
Assertion	bnj89	⊢ ( [ 𝑍 / 𝑦 ] ∃! 𝑥 𝜑 ↔ ∃! 𝑥 [ 𝑍 / 𝑦 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		bnj89.1	⊢ 𝑍 ∈ V
2		sbcex2	⊢ ( [ 𝑍 / 𝑦 ] ∃ 𝑤 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ∃ 𝑤 [ 𝑍 / 𝑦 ] ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) )
3		sbcal	⊢ ( [ 𝑍 / 𝑦 ] ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ∀ 𝑥 [ 𝑍 / 𝑦 ] ( 𝜑 ↔ 𝑥 = 𝑤 ) )
4	3	exbii	⊢ ( ∃ 𝑤 [ 𝑍 / 𝑦 ] ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ∃ 𝑤 ∀ 𝑥 [ 𝑍 / 𝑦 ] ( 𝜑 ↔ 𝑥 = 𝑤 ) )
5		sbcbig	⊢ ( 𝑍 ∈ V → ( [ 𝑍 / 𝑦 ] ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ( [ 𝑍 / 𝑦 ] 𝜑 ↔ [ 𝑍 / 𝑦 ] 𝑥 = 𝑤 ) ) )
6	1 5	ax-mp	⊢ ( [ 𝑍 / 𝑦 ] ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ( [ 𝑍 / 𝑦 ] 𝜑 ↔ [ 𝑍 / 𝑦 ] 𝑥 = 𝑤 ) )
7		sbcg	⊢ ( 𝑍 ∈ V → ( [ 𝑍 / 𝑦 ] 𝑥 = 𝑤 ↔ 𝑥 = 𝑤 ) )
8	1 7	ax-mp	⊢ ( [ 𝑍 / 𝑦 ] 𝑥 = 𝑤 ↔ 𝑥 = 𝑤 )
9	8	bibi2i	⊢ ( ( [ 𝑍 / 𝑦 ] 𝜑 ↔ [ 𝑍 / 𝑦 ] 𝑥 = 𝑤 ) ↔ ( [ 𝑍 / 𝑦 ] 𝜑 ↔ 𝑥 = 𝑤 ) )
10	6 9	bitri	⊢ ( [ 𝑍 / 𝑦 ] ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ( [ 𝑍 / 𝑦 ] 𝜑 ↔ 𝑥 = 𝑤 ) )
11	10	albii	⊢ ( ∀ 𝑥 [ 𝑍 / 𝑦 ] ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ∀ 𝑥 ( [ 𝑍 / 𝑦 ] 𝜑 ↔ 𝑥 = 𝑤 ) )
12	11	exbii	⊢ ( ∃ 𝑤 ∀ 𝑥 [ 𝑍 / 𝑦 ] ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ∃ 𝑤 ∀ 𝑥 ( [ 𝑍 / 𝑦 ] 𝜑 ↔ 𝑥 = 𝑤 ) )
13	2 4 12	3bitri	⊢ ( [ 𝑍 / 𝑦 ] ∃ 𝑤 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ∃ 𝑤 ∀ 𝑥 ( [ 𝑍 / 𝑦 ] 𝜑 ↔ 𝑥 = 𝑤 ) )
14		eu6	⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑤 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) )
15	14	sbcbii	⊢ ( [ 𝑍 / 𝑦 ] ∃! 𝑥 𝜑 ↔ [ 𝑍 / 𝑦 ] ∃ 𝑤 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) )
16		eu6	⊢ ( ∃! 𝑥 [ 𝑍 / 𝑦 ] 𝜑 ↔ ∃ 𝑤 ∀ 𝑥 ( [ 𝑍 / 𝑦 ] 𝜑 ↔ 𝑥 = 𝑤 ) )
17	13 15 16	3bitr4i	⊢ ( [ 𝑍 / 𝑦 ] ∃! 𝑥 𝜑 ↔ ∃! 𝑥 [ 𝑍 / 𝑦 ] 𝜑 )