Metamath Proof Explorer


Theorem elabgt

Description: Membership in a class abstraction, using implicit substitution. (Closed theorem version of elabg .) (Contributed by NM, 7-Nov-2005) (Proof shortened by Andrew Salmon, 8-Jun-2011) Reduce axiom usage. (Revised by Gino Giotto, 12-Oct-2024)

Ref Expression
Assertion elabgt ABxx=AφψAx|φψ

Proof

Step Hyp Ref Expression
1 elab6g ABAx|φxx=Aφ
2 1 adantr ABxx=AφψAx|φxx=Aφ
3 elisset ABxx=A
4 biimp φψφψ
5 4 imim3i x=Aφψx=Aφx=Aψ
6 5 al2imi xx=Aφψxx=Aφxx=Aψ
7 19.23v xx=Aψxx=Aψ
8 6 7 syl6ib xx=Aφψxx=Aφxx=Aψ
9 8 com3r xx=Axx=Aφψxx=Aφψ
10 biimpr φψψφ
11 10 imim2i x=Aφψx=Aψφ
12 11 alimi xx=Aφψxx=Aψφ
13 bi2.04 x=Aψφψx=Aφ
14 13 albii xx=Aψφxψx=Aφ
15 19.21v xψx=Aφψxx=Aφ
16 14 15 sylbb xx=Aψφψxx=Aφ
17 12 16 syl xx=Aφψψxx=Aφ
18 17 a1i xx=Axx=Aφψψxx=Aφ
19 9 18 impbidd xx=Axx=Aφψxx=Aφψ
20 3 19 syl ABxx=Aφψxx=Aφψ
21 20 imp ABxx=Aφψxx=Aφψ
22 2 21 bitrd ABxx=AφψAx|φψ