Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mpt2mptxf Structured version   Unicode version

Theorem mpt2mptxf 27176
 Description: Express a two-argument function as a one-argument function, or vice-versa. In this version is not assumed to be constant w.r.t . (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Thierry Arnoux, 31-Mar-2018.)
Hypotheses
Ref Expression
mpt2mptxf.0
mpt2mptxf.1
mpt2mptxf.2
Assertion
Ref Expression
mpt2mptxf
Distinct variable groups:   ,,,   ,,   ,
Allowed substitution hints:   ()   (,,)   (,)

Proof of Theorem mpt2mptxf
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-mpt 4500 . 2
2 df-mpt2 6280 . . 3
3 eliunxp 5131 . . . . . . 7
43anbi1i 695 . . . . . 6
5 nfcv 2622 . . . . . . . . . 10
6 mpt2mptxf.1 . . . . . . . . . 10
75, 6nfeq 2633 . . . . . . . . 9
8719.41 1915 . . . . . . . 8
98exbii 1639 . . . . . . 7
10 nfcv 2622 . . . . . . . . 9
11 mpt2mptxf.0 . . . . . . . . 9
1210, 11nfeq 2633 . . . . . . . 8
131219.41 1915 . . . . . . 7
149, 13bitri 249 . . . . . 6
15 anass 649 . . . . . . . 8
16 mpt2mptxf.2 . . . . . . . . . . 11
1716eqeq2d 2474 . . . . . . . . . 10
1817anbi2d 703 . . . . . . . . 9
1918pm5.32i 637 . . . . . . . 8
2015, 19bitri 249 . . . . . . 7
21202exbii 1640 . . . . . 6
224, 14, 213bitr2i 273 . . . . 5
2322opabbii 4504 . . . 4
24 dfoprab2 6318 . . . 4
2523, 24eqtr4i 2492 . . 3
262, 25eqtr4i 2492 . 2
271, 26eqtr4i 2492 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1374  wex 1591   wcel 1762  wnfc 2608  csn 4020  cop 4026  ciun 4318  copab 4497   cmpt 4498   cxp 4990  coprab 6276   cmpt2 6277 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-iun 4320  df-opab 4499  df-mpt 4500  df-xp 4998  df-rel 4999  df-oprab 6279  df-mpt2 6280 This theorem is referenced by:  gsummpt2co  27420
 Copyright terms: Public domain W3C validator