Metamath Proof Explorer


Theorem or2expropbilem2

Description: Lemma 2 for or2expropbi and ich2exprop . (Contributed by AV, 16-Jul-2023)

Ref Expression
Assertion or2expropbilem2 a b A B = a b φ x y A B = x y [˙y / b]˙ [˙x / a]˙ φ

Proof

Step Hyp Ref Expression
1 nfv x A B = a b φ
2 nfv y A B = a b φ
3 nfv a A B = x y
4 nfcv _ a y
5 nfsbc1v a [˙x / a]˙ φ
6 4 5 nfsbcw a [˙y / b]˙ [˙x / a]˙ φ
7 3 6 nfan a A B = x y [˙y / b]˙ [˙x / a]˙ φ
8 nfv b A B = x y
9 nfsbc1v b [˙y / b]˙ [˙x / a]˙ φ
10 8 9 nfan b A B = x y [˙y / b]˙ [˙x / a]˙ φ
11 opeq12 a = x b = y a b = x y
12 11 eqeq2d a = x b = y A B = a b A B = x y
13 sbceq1a a = x φ [˙x / a]˙ φ
14 sbceq1a b = y [˙x / a]˙ φ [˙y / b]˙ [˙x / a]˙ φ
15 13 14 sylan9bb a = x b = y φ [˙y / b]˙ [˙x / a]˙ φ
16 12 15 anbi12d a = x b = y A B = a b φ A B = x y [˙y / b]˙ [˙x / a]˙ φ
17 1 2 7 10 16 cbvex2v a b A B = a b φ x y A B = x y [˙y / b]˙ [˙x / a]˙ φ