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

Metamath Proof Explorer

Theorem ceqsexg

Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 11-Oct-2004)

Ref Expression
Hypotheses ceqsexg.1 ⊢ Ⅎ 𝑥 𝜓
ceqsexg.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion ceqsexg ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 ceqsexg.1 ⊢ Ⅎ 𝑥 𝜓
2 ceqsexg.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3 nfe1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 )
4 3 1 nfbi ⊢ Ⅎ 𝑥 ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜓 )
5 ceqex ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
6 5 2 bibi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ↔ 𝜑 ) ↔ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜓 ) ) )
7 biid ⊢ ( 𝜑 ↔ 𝜑 )
8 4 6 7 vtoclg1f ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜓 ) )