ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpo2eqb Unicode version

Theorem mpo2eqb 5832
Description: Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 5830. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
mpo2eqb  |-  ( A. x  e.  A  A. y  e.  B  C  e.  V  ->  ( ( x  e.  A , 
y  e.  B  |->  C )  =  ( x  e.  A ,  y  e.  B  |->  D )  <->  A. x  e.  A  A. y  e.  B  C  =  D )
)
Distinct variable groups:    x, y, A   
y, B
Allowed substitution hints:    B( x)    C( x, y)    D( x, y)    V( x, y)

Proof of Theorem mpo2eqb
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 pm13.183 2790 . . . . . 6  |-  ( C  e.  V  ->  ( C  =  D  <->  A. z
( z  =  C  <-> 
z  =  D ) ) )
21ralimi 2467 . . . . 5  |-  ( A. y  e.  B  C  e.  V  ->  A. y  e.  B  ( C  =  D  <->  A. z ( z  =  C  <->  z  =  D ) ) )
3 ralbi 2536 . . . . 5  |-  ( A. y  e.  B  ( C  =  D  <->  A. z
( z  =  C  <-> 
z  =  D ) )  ->  ( A. y  e.  B  C  =  D  <->  A. y  e.  B  A. z ( z  =  C  <->  z  =  D ) ) )
42, 3syl 14 . . . 4  |-  ( A. y  e.  B  C  e.  V  ->  ( A. y  e.  B  C  =  D  <->  A. y  e.  B  A. z ( z  =  C  <->  z  =  D ) ) )
54ralimi 2467 . . 3  |-  ( A. x  e.  A  A. y  e.  B  C  e.  V  ->  A. x  e.  A  ( A. y  e.  B  C  =  D  <->  A. y  e.  B  A. z ( z  =  C  <->  z  =  D ) ) )
6 ralbi 2536 . . 3  |-  ( A. x  e.  A  ( A. y  e.  B  C  =  D  <->  A. y  e.  B  A. z
( z  =  C  <-> 
z  =  D ) )  ->  ( A. x  e.  A  A. y  e.  B  C  =  D  <->  A. x  e.  A  A. y  e.  B  A. z ( z  =  C  <->  z  =  D ) ) )
75, 6syl 14 . 2  |-  ( A. x  e.  A  A. y  e.  B  C  e.  V  ->  ( A. x  e.  A  A. y  e.  B  C  =  D  <->  A. x  e.  A  A. y  e.  B  A. z ( z  =  C  <->  z  =  D ) ) )
8 df-mpo 5731 . . . 4  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
9 df-mpo 5731 . . . 4  |-  ( x  e.  A ,  y  e.  B  |->  D )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  D
) }
108, 9eqeq12i 2126 . . 3  |-  ( ( x  e.  A , 
y  e.  B  |->  C )  =  ( x  e.  A ,  y  e.  B  |->  D )  <->  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  D ) } )
11 eqoprab2b 5781 . . 3  |-  ( {
<. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  D ) }  <->  A. x A. y A. z ( ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C )  <->  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  D
) ) )
12 pm5.32 446 . . . . . . 7  |-  ( ( ( x  e.  A  /\  y  e.  B
)  ->  ( z  =  C  <->  z  =  D ) )  <->  ( (
( x  e.  A  /\  y  e.  B
)  /\  z  =  C )  <->  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  D
) ) )
1312albii 1427 . . . . . 6  |-  ( A. z ( ( x  e.  A  /\  y  e.  B )  ->  (
z  =  C  <->  z  =  D ) )  <->  A. z
( ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C )  <->  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  D
) ) )
14 19.21v 1825 . . . . . 6  |-  ( A. z ( ( x  e.  A  /\  y  e.  B )  ->  (
z  =  C  <->  z  =  D ) )  <->  ( (
x  e.  A  /\  y  e.  B )  ->  A. z ( z  =  C  <->  z  =  D ) ) )
1513, 14bitr3i 185 . . . . 5  |-  ( A. z ( ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C
)  <->  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  D ) )  <->  ( (
x  e.  A  /\  y  e.  B )  ->  A. z ( z  =  C  <->  z  =  D ) ) )
16152albii 1428 . . . 4  |-  ( A. x A. y A. z
( ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C )  <->  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  D
) )  <->  A. x A. y ( ( x  e.  A  /\  y  e.  B )  ->  A. z
( z  =  C  <-> 
z  =  D ) ) )
17 r2al 2426 . . . 4  |-  ( A. x  e.  A  A. y  e.  B  A. z ( z  =  C  <->  z  =  D )  <->  A. x A. y
( ( x  e.  A  /\  y  e.  B )  ->  A. z
( z  =  C  <-> 
z  =  D ) ) )
1816, 17bitr4i 186 . . 3  |-  ( A. x A. y A. z
( ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C )  <->  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  D
) )  <->  A. x  e.  A  A. y  e.  B  A. z
( z  =  C  <-> 
z  =  D ) )
1910, 11, 183bitri 205 . 2  |-  ( ( x  e.  A , 
y  e.  B  |->  C )  =  ( x  e.  A ,  y  e.  B  |->  D )  <->  A. x  e.  A  A. y  e.  B  A. z ( z  =  C  <->  z  =  D ) )
207, 19syl6rbbr 198 1  |-  ( A. x  e.  A  A. y  e.  B  C  e.  V  ->  ( ( x  e.  A , 
y  e.  B  |->  C )  =  ( x  e.  A ,  y  e.  B  |->  D )  <->  A. x  e.  A  A. y  e.  B  C  =  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104   A.wal 1310    = wceq 1312    e. wcel 1461   A.wral 2388   {coprab 5727    e. cmpo 5728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089  ax-setind 4410
This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-fal 1318  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ne 2281  df-ral 2393  df-v 2657  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-oprab 5730  df-mpo 5731
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator