Theorem opkelopkabg 4245

Description: Kuratowski ordered pair membership in an abstraction of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.)

Hypotheses

Ref	Expression
opkelopkabg.1	|- A = {x | E.yE.z(x = <<y, z>> /\ ph)}
opkelopkabg.2	|- (y = B -> (ph <-> ps))
opkelopkabg.3	|- (z = C -> (ps <-> ch))

Assertion

Ref	Expression
opkelopkabg	|- ((B e. V /\ C e. W) -> (<<B, C>> e. A <-> ch))

Distinct variable groups:   y,A,z   x,B,y,z   x,C,y,z   ch,z   ph,x   ps,y   x,y,z

Allowed substitution hints:   ph(y,z)   ps(x,z)   ch(x,y)   A(x)   V(x,y,z)   W(x,y,z)

Proof of Theorem opkelopkabg

Step	Hyp	Ref	Expression
1		opkex 4113	. . 3 |- <<B, C>> e. _V
2		eqeq1 2359	. . . . . 6 |- (x = <<B, C>> -> (x = <<y, z>> <-> <<B, C>> = <<y, z>>))
3		eqcom 2355	. . . . . 6 |- (<<B, C>> = <<y, z>> <-> <<y, z>> = <<B, C>>)
4	2, 3	syl6bb 252	. . . . 5 |- (x = <<B, C>> -> (x = <<y, z>> <-> <<y, z>> = <<B, C>>))
5	4	anbi1d 685	. . . 4 |- (x = <<B, C>> -> ((x = <<y, z>> /\ ph) <-> (<<y, z>> = <<B, C>> /\ ph)))
6	5	2exbidv 1628	. . 3 |- (x = <<B, C>> -> (E.yE.z(x = <<y, z>> /\ ph) <-> E.yE.z(<<y, z>> = <<B, C>> /\ ph)))
7		opkelopkabg.1	. . 3 |- A = {x | E.yE.z(x = <<y, z>> /\ ph)}
8	1, 6, 7	elab2 2988	. 2 |- (<<B, C>> e. A <-> E.yE.z(<<y, z>> = <<B, C>> /\ ph))
9		elex 2867	. . 3 |- (B e. V -> B e. _V)
10		elex 2867	. . 3 |- (C e. W -> C e. _V)
11		vex 2862	. . . . . . . . . . 11 |- y e. _V
12		vex 2862	. . . . . . . . . . 11 |- z e. _V
13		opkthg 4131	. . . . . . . . . . 11 |- ((y e. _V /\ z e. _V /\ C e. _V) -> (<<y, z>> = <<B, C>> <-> (y = B /\ z = C)))
14	11, 12, 13	mp3an12 1267	. . . . . . . . . 10 |- (C e. _V -> (<<y, z>> = <<B, C>> <-> (y = B /\ z = C)))
15	14	adantl 452	. . . . . . . . 9 |- ((B e. _V /\ C e. _V) -> (<<y, z>> = <<B, C>> <-> (y = B /\ z = C)))
16	15	anbi1d 685	. . . . . . . 8 |- ((B e. _V /\ C e. _V) -> ((<<y, z>> = <<B, C>> /\ ph) <-> ((y = B /\ z = C) /\ ph)))
17		anass 630	. . . . . . . 8 |- (((y = B /\ z = C) /\ ph) <-> (y = B /\ (z = C /\ ph)))
18	16, 17	syl6bb 252	. . . . . . 7 |- ((B e. _V /\ C e. _V) -> ((<<y, z>> = <<B, C>> /\ ph) <-> (y = B /\ (z = C /\ ph))))
19	18	exbidv 1626	. . . . . 6 |- ((B e. _V /\ C e. _V) -> (E.z(<<y, z>> = <<B, C>> /\ ph) <-> E.z(y = B /\ (z = C /\ ph))))
20		19.42v 1905	. . . . . 6 |- (E.z(y = B /\ (z = C /\ ph)) <-> (y = B /\ E.z(z = C /\ ph)))
21	19, 20	syl6bb 252	. . . . 5 |- ((B e. _V /\ C e. _V) -> (E.z(<<y, z>> = <<B, C>> /\ ph) <-> (y = B /\ E.z(z = C /\ ph))))
22	21	exbidv 1626	. . . 4 |- ((B e. _V /\ C e. _V) -> (E.yE.z(<<y, z>> = <<B, C>> /\ ph) <-> E.y(y = B /\ E.z(z = C /\ ph))))
23		opkelopkabg.2	. . . . . . . 8 |- (y = B -> (ph <-> ps))
24	23	anbi2d 684	. . . . . . 7 |- (y = B -> ((z = C /\ ph) <-> (z = C /\ ps)))
25	24	exbidv 1626	. . . . . 6 |- (y = B -> (E.z(z = C /\ ph) <-> E.z(z = C /\ ps)))
26	25	ceqsexgv 2971	. . . . 5 |- (B e. _V -> (E.y(y = B /\ E.z(z = C /\ ph)) <-> E.z(z = C /\ ps)))
27	26	adantr 451	. . . 4 |- ((B e. _V /\ C e. _V) -> (E.y(y = B /\ E.z(z = C /\ ph)) <-> E.z(z = C /\ ps)))
28		opkelopkabg.3	. . . . . 6 |- (z = C -> (ps <-> ch))
29	28	ceqsexgv 2971	. . . . 5 |- (C e. _V -> (E.z(z = C /\ ps) <-> ch))
30	29	adantl 452	. . . 4 |- ((B e. _V /\ C e. _V) -> (E.z(z = C /\ ps) <-> ch))
31	22, 27, 30	3bitrd 270	. . 3 |- ((B e. _V /\ C e. _V) -> (E.yE.z(<<y, z>> = <<B, C>> /\ ph) <-> ch))
32	9, 10, 31	syl2an 463	. 2 |- ((B e. V /\ C e. W) -> (E.yE.z(<<y, z>> = <<B, C>> /\ ph) <-> ch))
33	8, 32	syl5bb 248	1 |- ((B e. V /\ C e. W) -> (<<B, C>> e. A <-> ch))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358  E.wex 1541   = wceq 1642   e. wcel 1710  {cab 2339  _Vcvv 2859  <<copk 4057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-sn 4087

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551  df-sn 3741  df-pr 3742  df-opk 4058

This theorem is referenced by:  opkelopkab  4246  opkelxpkg  4247  opkelcnvkg  4249  opkelins2kg  4251  opkelins3kg  4252  opkelsikg  4264  opkelssetkg  4268  opkelidkg  4274  opklefing  4448  opkltfing  4449