Metamath Proof Explorer

Theorem csbxpgVD

Description: Virtual deduction proof of csbxp . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbxp is csbxpgVD without virtual deductions and was automatically derived from csbxpgVD .

1:: |- (. A e. V ->. A e. V ).
2:1: |- (. A e. V ->. ( [. A / x ]. w e. B <-> [_ A / x ]_ w e. [_ A / x ]_ B ) ).
3:1: |- (. A e. V ->. [_ A / x ]_ w = w ).
4:3: |- (. A e. V ->. ( [_ A / x ]_ w e. [_ A / x ]_ B <-> w e. [_ A / x ]_ B ) ).
5:2,4: |- (. A e. V ->. ( [. A / x ]. w e. B <-> w e. [_ A / x ]_ B ) ).
6:1: |- (. A e. V ->. ( [. A / x ]. y e. C <-> [_ A / x ]_ y e. [_ A / x ]_ C ) ).
7:1: |- (. A e. V ->. [_ A / x ]_ y = y ).
8:7: |- (. A e. V ->. ( [_ A / x ]_ y e. [_ A / x ]_ C <-> y e. [_ A / x ]_ C ) ).
9:6,8: |- (. A e. V ->. ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) ).
10:5,9: |- (. A e. V ->. ( ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ).
11:1: |- (. A e. V ->. ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) ) ).
12:10,11: |- (. A e. V ->. ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ).
13:1: |- (. A e. V ->. ( [. A / x ]. z = <. w ,. y >. <-> z = <. w , y >. ) ).
14:12,13: |- (. A e. V ->. ( ( [. A / x ]. z = <. w ,. y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
15:1: |- (. A e. V ->. ( [. A / x ]. ( z = <. w ,. y >. /\ ( w e. B /\ y e. C ) ) <-> ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) ) ).
16:14,15: |- (. A e. V ->. ( [. A / x ]. ( z = <. w ,. y >. /\ ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
17:16: |- (. A e. V ->. A. y ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
18:17: |- (. A e. V ->. ( E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
19:1: |- (. A e. V ->. ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) ).
20:18,19: |- (. A e. V ->. ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
21:20: |- (. A e. V ->. A. w ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
22:21: |- (. A e. V ->. ( E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
23:1: |- (. A e. V ->. ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) ).
24:22,23: |- (. A e. V ->. ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
25:24: |- (. A e. V ->. A. z ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
26:25: |- (. A e. V ->. { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ).
27:1: |- (. A e. V ->. [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } ).
28:26,27: |- (. A e. V ->. [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ).
29:: |- { <. w ,. y >. | ( w e. B /\ y e. C ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
30:: |- ( B X. C ) = { <. w ,. y >. | ( w e. B /\ y e. C ) }
31:29,30: |- ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
32:31: |- A. x ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
33:1,32: |- (. A e. V ->. [_ A / x ]_ ( B X. C ) = [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } ).
34:28,33: |- (. A e. V ->. [_ A / x ]_ ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ).
35:: |- { <. w ,. y >. | ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) }
36:: |- ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { <. w , y >. | ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) }
37:35,36: |- ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) }
38:34,37: |- (. A e. V ->. [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) ).
qed:38: |- ( A e. V -> [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) )
(Contributed by Alan Sare, 10-Nov-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion csbxpgVD ⊢A∈V→⦋A/x⦌B×C=⦋A/x⦌B×⦋A/x⦌C

Proof

Step Hyp Ref Expression
1 idn1 ⊢A∈V→A∈V
2 sbcel12 ⊢[˙A/x]˙w∈B↔⦋A/x⦌w∈⦋A/x⦌B
3 2 a1i ⊢A∈V→[˙A/x]˙w∈B↔⦋A/x⦌w∈⦋A/x⦌B
4 1 3 e1a ⊢A∈V→[˙A/x]˙w∈B↔⦋A/x⦌w∈⦋A/x⦌B
5 csbconstg ⊢A∈V→⦋A/x⦌w=w
6 1 5 e1a ⊢A∈V→⦋A/x⦌w=w
7 eleq1 ⊢⦋A/x⦌w=w→⦋A/x⦌w∈⦋A/x⦌B↔w∈⦋A/x⦌B
8 6 7 e1a ⊢A∈V→⦋A/x⦌w∈⦋A/x⦌B↔w∈⦋A/x⦌B
9 bibi1 ⊢[˙A/x]˙w∈B↔⦋A/x⦌w∈⦋A/x⦌B→[˙A/x]˙w∈B↔w∈⦋A/x⦌B↔⦋A/x⦌w∈⦋A/x⦌B↔w∈⦋A/x⦌B
10 9 biimprd ⊢[˙A/x]˙w∈B↔⦋A/x⦌w∈⦋A/x⦌B→⦋A/x⦌w∈⦋A/x⦌B↔w∈⦋A/x⦌B→[˙A/x]˙w∈B↔w∈⦋A/x⦌B
11 4 8 10 e11 ⊢A∈V→[˙A/x]˙w∈B↔w∈⦋A/x⦌B
12 sbcel12 ⊢[˙A/x]˙y∈C↔⦋A/x⦌y∈⦋A/x⦌C
13 12 a1i ⊢A∈V→[˙A/x]˙y∈C↔⦋A/x⦌y∈⦋A/x⦌C
14 1 13 e1a ⊢A∈V→[˙A/x]˙y∈C↔⦋A/x⦌y∈⦋A/x⦌C
15 csbconstg ⊢A∈V→⦋A/x⦌y=y
16 1 15 e1a ⊢A∈V→⦋A/x⦌y=y
17 eleq1 ⊢⦋A/x⦌y=y→⦋A/x⦌y∈⦋A/x⦌C↔y∈⦋A/x⦌C
18 16 17 e1a ⊢A∈V→⦋A/x⦌y∈⦋A/x⦌C↔y∈⦋A/x⦌C
19 bibi1 ⊢[˙A/x]˙y∈C↔⦋A/x⦌y∈⦋A/x⦌C→[˙A/x]˙y∈C↔y∈⦋A/x⦌C↔⦋A/x⦌y∈⦋A/x⦌C↔y∈⦋A/x⦌C
20 19 biimprd ⊢[˙A/x]˙y∈C↔⦋A/x⦌y∈⦋A/x⦌C→⦋A/x⦌y∈⦋A/x⦌C↔y∈⦋A/x⦌C→[˙A/x]˙y∈C↔y∈⦋A/x⦌C
21 14 18 20 e11 ⊢A∈V→[˙A/x]˙y∈C↔y∈⦋A/x⦌C
22 pm4.38 ⊢[˙A/x]˙w∈B↔w∈⦋A/x⦌B∧[˙A/x]˙y∈C↔y∈⦋A/x⦌C→[˙A/x]˙w∈B∧[˙A/x]˙y∈C↔w∈⦋A/x⦌B∧y∈⦋A/x⦌C
23 22 ex ⊢[˙A/x]˙w∈B↔w∈⦋A/x⦌B→[˙A/x]˙y∈C↔y∈⦋A/x⦌C→[˙A/x]˙w∈B∧[˙A/x]˙y∈C↔w∈⦋A/x⦌B∧y∈⦋A/x⦌C
24 11 21 23 e11 ⊢A∈V→[˙A/x]˙w∈B∧[˙A/x]˙y∈C↔w∈⦋A/x⦌B∧y∈⦋A/x⦌C
25 sbcan ⊢[˙A/x]˙w∈B∧y∈C↔[˙A/x]˙w∈B∧[˙A/x]˙y∈C
26 25 a1i ⊢A∈V→[˙A/x]˙w∈B∧y∈C↔[˙A/x]˙w∈B∧[˙A/x]˙y∈C
27 1 26 e1a ⊢A∈V→[˙A/x]˙w∈B∧y∈C↔[˙A/x]˙w∈B∧[˙A/x]˙y∈C
28 bibi1 ⊢[˙A/x]˙w∈B∧y∈C↔[˙A/x]˙w∈B∧[˙A/x]˙y∈C→[˙A/x]˙w∈B∧y∈C↔w∈⦋A/x⦌B∧y∈⦋A/x⦌C↔[˙A/x]˙w∈B∧[˙A/x]˙y∈C↔w∈⦋A/x⦌B∧y∈⦋A/x⦌C
29 28 biimprcd ⊢[˙A/x]˙w∈B∧[˙A/x]˙y∈C↔w∈⦋A/x⦌B∧y∈⦋A/x⦌C→[˙A/x]˙w∈B∧y∈C↔[˙A/x]˙w∈B∧[˙A/x]˙y∈C→[˙A/x]˙w∈B∧y∈C↔w∈⦋A/x⦌B∧y∈⦋A/x⦌C
30 24 27 29 e11 ⊢A∈V→[˙A/x]˙w∈B∧y∈C↔w∈⦋A/x⦌B∧y∈⦋A/x⦌C
31 sbcg ⊢A∈V→[˙A/x]˙z=wy↔z=wy
32 1 31 e1a ⊢A∈V→[˙A/x]˙z=wy↔z=wy
33 pm4.38 ⊢[˙A/x]˙z=wy↔z=wy∧[˙A/x]˙w∈B∧y∈C↔w∈⦋A/x⦌B∧y∈⦋A/x⦌C→[˙A/x]˙z=wy∧[˙A/x]˙w∈B∧y∈C↔z=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
34 33 expcom ⊢[˙A/x]˙w∈B∧y∈C↔w∈⦋A/x⦌B∧y∈⦋A/x⦌C→[˙A/x]˙z=wy↔z=wy→[˙A/x]˙z=wy∧[˙A/x]˙w∈B∧y∈C↔z=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
35 30 32 34 e11 ⊢A∈V→[˙A/x]˙z=wy∧[˙A/x]˙w∈B∧y∈C↔z=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
36 sbcan ⊢[˙A/x]˙z=wy∧w∈B∧y∈C↔[˙A/x]˙z=wy∧[˙A/x]˙w∈B∧y∈C
37 36 a1i ⊢A∈V→[˙A/x]˙z=wy∧w∈B∧y∈C↔[˙A/x]˙z=wy∧[˙A/x]˙w∈B∧y∈C
38 1 37 e1a ⊢A∈V→[˙A/x]˙z=wy∧w∈B∧y∈C↔[˙A/x]˙z=wy∧[˙A/x]˙w∈B∧y∈C
39 bibi1 ⊢[˙A/x]˙z=wy∧w∈B∧y∈C↔[˙A/x]˙z=wy∧[˙A/x]˙w∈B∧y∈C→[˙A/x]˙z=wy∧w∈B∧y∈C↔z=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C↔[˙A/x]˙z=wy∧[˙A/x]˙w∈B∧y∈C↔z=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
40 39 biimprcd ⊢[˙A/x]˙z=wy∧[˙A/x]˙w∈B∧y∈C↔z=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C→[˙A/x]˙z=wy∧w∈B∧y∈C↔[˙A/x]˙z=wy∧[˙A/x]˙w∈B∧y∈C→[˙A/x]˙z=wy∧w∈B∧y∈C↔z=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
41 35 38 40 e11 ⊢A∈V→[˙A/x]˙z=wy∧w∈B∧y∈C↔z=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
42 41 gen11 ⊢A∈V→∀y[˙A/x]˙z=wy∧w∈B∧y∈C↔z=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
43 exbi ⊢∀y[˙A/x]˙z=wy∧w∈B∧y∈C↔z=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C→∃y[˙A/x]˙z=wy∧w∈B∧y∈C↔∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
44 42 43 e1a ⊢A∈V→∃y[˙A/x]˙z=wy∧w∈B∧y∈C↔∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
45 sbcex2 ⊢[˙A/x]˙∃yz=wy∧w∈B∧y∈C↔∃y[˙A/x]˙z=wy∧w∈B∧y∈C
46 45 a1i ⊢A∈V→[˙A/x]˙∃yz=wy∧w∈B∧y∈C↔∃y[˙A/x]˙z=wy∧w∈B∧y∈C
47 1 46 e1a ⊢A∈V→[˙A/x]˙∃yz=wy∧w∈B∧y∈C↔∃y[˙A/x]˙z=wy∧w∈B∧y∈C
48 bibi1 ⊢[˙A/x]˙∃yz=wy∧w∈B∧y∈C↔∃y[˙A/x]˙z=wy∧w∈B∧y∈C→[˙A/x]˙∃yz=wy∧w∈B∧y∈C↔∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C↔∃y[˙A/x]˙z=wy∧w∈B∧y∈C↔∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
49 48 biimprcd ⊢∃y[˙A/x]˙z=wy∧w∈B∧y∈C↔∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C→[˙A/x]˙∃yz=wy∧w∈B∧y∈C↔∃y[˙A/x]˙z=wy∧w∈B∧y∈C→[˙A/x]˙∃yz=wy∧w∈B∧y∈C↔∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
50 44 47 49 e11 ⊢A∈V→[˙A/x]˙∃yz=wy∧w∈B∧y∈C↔∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
51 50 gen11 ⊢A∈V→∀w[˙A/x]˙∃yz=wy∧w∈B∧y∈C↔∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
52 exbi ⊢∀w[˙A/x]˙∃yz=wy∧w∈B∧y∈C↔∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C→∃w[˙A/x]˙∃yz=wy∧w∈B∧y∈C↔∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
53 51 52 e1a ⊢A∈V→∃w[˙A/x]˙∃yz=wy∧w∈B∧y∈C↔∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
54 sbcex2 ⊢[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C↔∃w[˙A/x]˙∃yz=wy∧w∈B∧y∈C
55 54 a1i ⊢A∈V→[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C↔∃w[˙A/x]˙∃yz=wy∧w∈B∧y∈C
56 1 55 e1a ⊢A∈V→[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C↔∃w[˙A/x]˙∃yz=wy∧w∈B∧y∈C
57 bibi1 ⊢[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C↔∃w[˙A/x]˙∃yz=wy∧w∈B∧y∈C→[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C↔∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C↔∃w[˙A/x]˙∃yz=wy∧w∈B∧y∈C↔∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
58 57 biimprcd ⊢∃w[˙A/x]˙∃yz=wy∧w∈B∧y∈C↔∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C→[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C↔∃w[˙A/x]˙∃yz=wy∧w∈B∧y∈C→[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C↔∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
59 53 56 58 e11 ⊢A∈V→[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C↔∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
60 59 gen11 ⊢A∈V→∀z[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C↔∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
61 abbib ⊢z|[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C↔∀z[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C↔∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
62 61 biimpri ⊢∀z[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C↔∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C→z|[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
63 60 62 e1a ⊢A∈V→z|[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
64 csbab ⊢⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C=z|[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C
65 64 a1i ⊢A∈V→⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C=z|[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C
66 1 65 e1a ⊢A∈V→⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C=z|[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C
67 eqeq2 ⊢z|[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C→⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C=z|[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C↔⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
68 67 biimpd ⊢z|[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C→⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C=z|[˙A/x]˙∃w∃yz=wy∧w∈B∧y∈C→⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
69 63 66 68 e11 ⊢A∈V→⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
70 df-xp ⊢B×C=wy|w∈B∧y∈C
71 df-opab ⊢wy|w∈B∧y∈C=z|∃w∃yz=wy∧w∈B∧y∈C
72 70 71 eqtri ⊢B×C=z|∃w∃yz=wy∧w∈B∧y∈C
73 72 ax-gen ⊢∀xB×C=z|∃w∃yz=wy∧w∈B∧y∈C
74 csbeq2 ⊢∀xB×C=z|∃w∃yz=wy∧w∈B∧y∈C→⦋A/x⦌B×C=⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C
75 74 a1i ⊢A∈V→∀xB×C=z|∃w∃yz=wy∧w∈B∧y∈C→⦋A/x⦌B×C=⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C
76 1 73 75 e10 ⊢A∈V→⦋A/x⦌B×C=⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C
77 eqeq2 ⊢⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C→⦋A/x⦌B×C=⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C↔⦋A/x⦌B×C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
78 77 biimpd ⊢⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C→⦋A/x⦌B×C=⦋A/x⦌z|∃w∃yz=wy∧w∈B∧y∈C→⦋A/x⦌B×C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
79 69 76 78 e11 ⊢A∈V→⦋A/x⦌B×C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
80 df-xp ⊢⦋A/x⦌B×⦋A/x⦌C=wy|w∈⦋A/x⦌B∧y∈⦋A/x⦌C
81 df-opab ⊢wy|w∈⦋A/x⦌B∧y∈⦋A/x⦌C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
82 80 81 eqtri ⊢⦋A/x⦌B×⦋A/x⦌C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
83 eqeq2 ⊢⦋A/x⦌B×⦋A/x⦌C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C→⦋A/x⦌B×C=⦋A/x⦌B×⦋A/x⦌C↔⦋A/x⦌B×C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C
84 83 biimprcd ⊢⦋A/x⦌B×C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C→⦋A/x⦌B×⦋A/x⦌C=z|∃w∃yz=wy∧w∈⦋A/x⦌B∧y∈⦋A/x⦌C→⦋A/x⦌B×C=⦋A/x⦌B×⦋A/x⦌C
85 79 82 84 e10 ⊢A∈V→⦋A/x⦌B×C=⦋A/x⦌B×⦋A/x⦌C
86 85 in1 ⊢A∈V→⦋A/x⦌B×C=⦋A/x⦌B×⦋A/x⦌C