This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( [ 𝑍 / 𝑦 ] ∃! 𝑥 𝜑 ↔ ∃! 𝑥 [ 𝑍 / 𝑦 ] 𝜑 )