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

Metamath Proof Explorer

Theorem sbcoreleleq

Description: Substitution of a setvar variable for another setvar variable in a 3-conjunct formula. Derived automatically from sbcoreleleqVD . (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sbcoreleleq ⊢ A ∈ V → [˙A / y]˙ x ∈ y ∨ y ∈ x ∨ x = y ↔ x ∈ A ∨ A ∈ x ∨ x = A

Proof

Step Hyp Ref Expression
1 sbc3or ⊢ [˙A / y]˙ x ∈ y ∨ y ∈ x ∨ x = y ↔ [˙A / y]˙ x ∈ y ∨ [˙A / y]˙ y ∈ x ∨ [˙A / y]˙ x = y
2 sbcel2gv ⊢ A ∈ V → [˙A / y]˙ x ∈ y ↔ x ∈ A
3 sbcel1v ⊢ [˙A / y]˙ y ∈ x ↔ A ∈ x
4 3 a1i ⊢ A ∈ V → [˙A / y]˙ y ∈ x ↔ A ∈ x
5 eqsbc2 ⊢ A ∈ V → [˙A / y]˙ x = y ↔ x = A
6 3orbi123 ⊢ [˙A / y]˙ x ∈ y ↔ x ∈ A ∧ [˙A / y]˙ y ∈ x ↔ A ∈ x ∧ [˙A / y]˙ x = y ↔ x = A → [˙A / y]˙ x ∈ y ∨ [˙A / y]˙ y ∈ x ∨ [˙A / y]˙ x = y ↔ x ∈ A ∨ A ∈ x ∨ x = A
7 6 3impexpbicomi ⊢ [˙A / y]˙ x ∈ y ↔ x ∈ A → [˙A / y]˙ y ∈ x ↔ A ∈ x → [˙A / y]˙ x = y ↔ x = A → x ∈ A ∨ A ∈ x ∨ x = A ↔ [˙A / y]˙ x ∈ y ∨ [˙A / y]˙ y ∈ x ∨ [˙A / y]˙ x = y
8 2 4 5 7 syl3c ⊢ A ∈ V → x ∈ A ∨ A ∈ x ∨ x = A ↔ [˙A / y]˙ x ∈ y ∨ [˙A / y]˙ y ∈ x ∨ [˙A / y]˙ x = y
9 1 8 bitr4id ⊢ A ∈ V → [˙A / y]˙ x ∈ y ∨ y ∈ x ∨ x = y ↔ x ∈ A ∨ A ∈ x ∨ x = A