eleq2s - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > eleq2s		Unicode version

Theorem eleq2s 2445

Description: Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

**Hypotheses**
Ref	Expression
eleq2s.1
eleq2s.2

**Assertion**
Ref	Expression
eleq2s

**Proof of Theorem eleq2s**
Step	Hyp	Ref	Expression
1		eleq2s.2	. . 3
2	1	eleq2i 2417	. 2
3		eleq2s.1	. 2
4	2, 3	sylbi 187	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1642

wcel 1710

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746 ax-ext 2334

This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-cleq 2346 df-clel 2349

This theorem is referenced by: elxpi 4800 optocl 4838 ecexr 5950 ectocld 5991 ecoptocl 5996 nulnnc 6118 ncprc 6124 elnc 6125