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

Metamath Proof Explorer

Theorem sbc7

Description: An equivalence for class substitution in the spirit of df-clab . Note that x and A don't have to be distinct. (Contributed by NM, 18-Nov-2008) (Revised by Mario Carneiro, 13-Oct-2016)

		Ref	Expression
	Assertion	sbc7	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		sbccow	⊢ ( [ 𝐴 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 )
2		sbc5	⊢ ( [ 𝐴 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
3	1 2	bitr3i	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )