Metamath Proof Explorer


Theorem sbss

Description: Set substitution into the first argument of a subset relation. (Contributed by Rodolfo Medina, 7-Jul-2010) (Proof shortened by Mario Carneiro, 14-Nov-2016)

Ref Expression
Assertion sbss yxxAyA

Proof

Step Hyp Ref Expression
1 sseq1 x=zxAzA
2 sseq1 z=yzAyA
3 1 2 sbievw2 yxxAyA