Metamath Proof Explorer


Theorem axc11r

Description: Same as axc11 but with reversed antecedent. Note the use of ax-12 (and not merely ax12v as in axc11rv ).

This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev and aecom , for example) in proofs. In practice, theorems beyond elementary set theory do not really benefit from such eliminations. As of 2024, it is used in conjunction with ax-13 only, and like that, it should be applied only in niches where indispensable. (Contributed by NM, 25-Jul-2015)

Ref Expression
Assertion axc11r yy=xxφyφ

Proof

Step Hyp Ref Expression
1 ax-12 y=xxφyy=xφ
2 1 sps yy=xxφyy=xφ
3 pm2.27 y=xy=xφφ
4 3 al2imi yy=xyy=xφyφ
5 2 4 syld yy=xxφyφ