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

Metamath Proof Explorer

Theorem bnj610

Description: Pass from equality ( x = A ) to substitution ( [. A / x ]. ) without the distinct variable condition on A , x . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj610.1 ⊢ A ∈ V
bnj610.2 ⊢ x = A → φ ↔ ψ
bnj610.3 No typesetting found for |- ( x = y -> ( ph <-> ps' ) ) with typecode |-
bnj610.4 No typesetting found for |- ( y = A -> ( ps' <-> ps ) ) with typecode |-
Assertion bnj610 ⊢ [˙A / x]˙ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 bnj610.1 ⊢ A ∈ V
2 bnj610.2 ⊢ x = A → φ ↔ ψ
3 bnj610.3 Could not format ( x = y -> ( ph <-> ps' ) ) : No typesetting found for |- ( x = y -> ( ph <-> ps' ) ) with typecode |-
4 bnj610.4 Could not format ( y = A -> ( ps' <-> ps ) ) : No typesetting found for |- ( y = A -> ( ps' <-> ps ) ) with typecode |-
5 vex ⊢ y ∈ V
6 5 3 sbcie Could not format ( [. y / x ]. ph <-> ps' ) : No typesetting found for |- ( [. y / x ]. ph <-> ps' ) with typecode |-
7 6 sbcbii Could not format ( [. A / y ]. [. y / x ]. ph <-> [. A / y ]. ps' ) : No typesetting found for |- ( [. A / y ]. [. y / x ]. ph <-> [. A / y ]. ps' ) with typecode |-
8 sbccow ⊢ [˙A / y]˙ [˙y / x]˙ φ ↔ [˙A / x]˙ φ
9 1 4 sbcie Could not format ( [. A / y ]. ps' <-> ps ) : No typesetting found for |- ( [. A / y ]. ps' <-> ps ) with typecode |-
10 7 8 9 3bitr3i ⊢ [˙A / x]˙ φ ↔ ψ