Metamath Proof Explorer

Theorem eqvinot

Description: A variable introduction law for ordered triples, analogous to eqvinop . (Contributed by BTernaryTau, 8-Sep-2026)

Ref Expression
Hypotheses eqvinot.1 
|- B e. _V
eqvinot.2 
|- C e. _V
eqvinot.3 
|- D e. _V
Assertion eqvinot 
|- ( A = <. B , C , D >. <-> E. x E. y E. z ( A = <. x , y , z >. /\ <. x , y , z >. = <. B , C , D >. ) )

Proof

Step Hyp Ref Expression
1 eqvinot.1 
 |-  B e. _V
2 eqvinot.2 
 |-  C e. _V
3 eqvinot.3 
 |-  D e. _V
4 19.42v 
 |-  ( E. y ( x = B /\ ( y = C /\ A = <. x , y , D >. ) ) <-> ( x = B /\ E. y ( y = C /\ A = <. x , y , D >. ) ) )
5 19.42v 
 |-  ( E. z ( ( x = B /\ y = C ) /\ ( z = D /\ A = <. x , y , z >. ) ) <-> ( ( x = B /\ y = C ) /\ E. z ( z = D /\ A = <. x , y , z >. ) ) )
6 vex 
 |-  x e. _V
7 vex 
 |-  y e. _V
8 vex 
 |-  z e. _V
9 6 7 8 otth 
 |-  ( <. x , y , z >. = <. B , C , D >. <-> ( x = B /\ y = C /\ z = D ) )
10 9 anbi2i 
 |-  ( ( A = <. x , y , z >. /\ <. x , y , z >. = <. B , C , D >. ) <-> ( A = <. x , y , z >. /\ ( x = B /\ y = C /\ z = D ) ) )
11 ancom 
 |-  ( ( A = <. x , y , z >. /\ ( x = B /\ y = C /\ z = D ) ) <-> ( ( x = B /\ y = C /\ z = D ) /\ A = <. x , y , z >. ) )
12 3an4anass 
 |-  ( ( ( x = B /\ y = C /\ z = D ) /\ A = <. x , y , z >. ) <-> ( ( x = B /\ y = C ) /\ ( z = D /\ A = <. x , y , z >. ) ) )
13 10 11 12 3bitrri 
 |-  ( ( ( x = B /\ y = C ) /\ ( z = D /\ A = <. x , y , z >. ) ) <-> ( A = <. x , y , z >. /\ <. x , y , z >. = <. B , C , D >. ) )
14 13 exbii 
 |-  ( E. z ( ( x = B /\ y = C ) /\ ( z = D /\ A = <. x , y , z >. ) ) <-> E. z ( A = <. x , y , z >. /\ <. x , y , z >. = <. B , C , D >. ) )
15 oteq3 
 |-  ( z = D -> <. x , y , z >. = <. x , y , D >. )
16 15 eqeq2d 
 |-  ( z = D -> ( A = <. x , y , z >. <-> A = <. x , y , D >. ) )
17 3 16 ceqsexv 
 |-  ( E. z ( z = D /\ A = <. x , y , z >. ) <-> A = <. x , y , D >. )
18 17 anbi2i 
 |-  ( ( ( x = B /\ y = C ) /\ E. z ( z = D /\ A = <. x , y , z >. ) ) <-> ( ( x = B /\ y = C ) /\ A = <. x , y , D >. ) )
19 5 14 18 3bitr3i 
 |-  ( E. z ( A = <. x , y , z >. /\ <. x , y , z >. = <. B , C , D >. ) <-> ( ( x = B /\ y = C ) /\ A = <. x , y , D >. ) )
20 anass 
 |-  ( ( ( x = B /\ y = C ) /\ A = <. x , y , D >. ) <-> ( x = B /\ ( y = C /\ A = <. x , y , D >. ) ) )
21 19 20 bitr2i 
 |-  ( ( x = B /\ ( y = C /\ A = <. x , y , D >. ) ) <-> E. z ( A = <. x , y , z >. /\ <. x , y , z >. = <. B , C , D >. ) )
22 21 exbii 
 |-  ( E. y ( x = B /\ ( y = C /\ A = <. x , y , D >. ) ) <-> E. y E. z ( A = <. x , y , z >. /\ <. x , y , z >. = <. B , C , D >. ) )
23 oteq2 
 |-  ( y = C -> <. x , y , D >. = <. x , C , D >. )
24 23 eqeq2d 
 |-  ( y = C -> ( A = <. x , y , D >. <-> A = <. x , C , D >. ) )
25 2 24 ceqsexv 
 |-  ( E. y ( y = C /\ A = <. x , y , D >. ) <-> A = <. x , C , D >. )
26 25 anbi2i 
 |-  ( ( x = B /\ E. y ( y = C /\ A = <. x , y , D >. ) ) <-> ( x = B /\ A = <. x , C , D >. ) )
27 4 22 26 3bitr3i 
 |-  ( E. y E. z ( A = <. x , y , z >. /\ <. x , y , z >. = <. B , C , D >. ) <-> ( x = B /\ A = <. x , C , D >. ) )
28 27 exbii 
 |-  ( E. x E. y E. z ( A = <. x , y , z >. /\ <. x , y , z >. = <. B , C , D >. ) <-> E. x ( x = B /\ A = <. x , C , D >. ) )
29 oteq1 
 |-  ( x = B -> <. x , C , D >. = <. B , C , D >. )
30 29 eqeq2d 
 |-  ( x = B -> ( A = <. x , C , D >. <-> A = <. B , C , D >. ) )
31 1 30 ceqsexv 
 |-  ( E. x ( x = B /\ A = <. x , C , D >. ) <-> A = <. B , C , D >. )
32 28 31 bitr2i 
 |-  ( A = <. B , C , D >. <-> E. x E. y E. z ( A = <. x , y , z >. /\ <. x , y , z >. = <. B , C , D >. ) )