MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfoprab2 Structured version   Visualization version   GIF version

Theorem dfoprab2 6666
Description: Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.)
Assertion
Ref Expression
dfoprab2 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Distinct variable groups:   𝑥,𝑧,𝑤   𝑦,𝑧,𝑤   𝜑,𝑤
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem dfoprab2
Dummy variable 𝑣 is distinct from all other variables.
StepHypRef Expression
1 excom 2039 . . . 4 (∃𝑧𝑤𝑥𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑤𝑧𝑥𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
2 exrot4 2043 . . . . 5 (∃𝑧𝑤𝑥𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑥𝑦𝑧𝑤(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
3 opeq1 4377 . . . . . . . . . . . 12 (𝑤 = ⟨𝑥, 𝑦⟩ → ⟨𝑤, 𝑧⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
43eqeq2d 2631 . . . . . . . . . . 11 (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑣 = ⟨𝑤, 𝑧⟩ ↔ 𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
54pm5.32ri 669 . . . . . . . . . 10 ((𝑣 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩))
65anbi1i 730 . . . . . . . . 9 (((𝑣 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ∧ 𝜑) ↔ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ∧ 𝜑))
7 anass 680 . . . . . . . . 9 (((𝑣 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ∧ 𝜑) ↔ (𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
8 an32 838 . . . . . . . . 9 (((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ∧ 𝜑) ↔ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩))
96, 7, 83bitr3i 290 . . . . . . . 8 ((𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩))
109exbii 1771 . . . . . . 7 (∃𝑤(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑤((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩))
11 opex 4903 . . . . . . . . 9 𝑥, 𝑦⟩ ∈ V
1211isseti 3199 . . . . . . . 8 𝑤 𝑤 = ⟨𝑥, 𝑦
13 19.42v 1915 . . . . . . . 8 (∃𝑤((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ↔ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ ∃𝑤 𝑤 = ⟨𝑥, 𝑦⟩))
1412, 13mpbiran2 953 . . . . . . 7 (∃𝑤((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
1510, 14bitri 264 . . . . . 6 (∃𝑤(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
16153exbii 1773 . . . . 5 (∃𝑥𝑦𝑧𝑤(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑥𝑦𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
172, 16bitri 264 . . . 4 (∃𝑧𝑤𝑥𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑥𝑦𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
18 19.42vv 1917 . . . . 5 (∃𝑥𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ (𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
19182exbii 1772 . . . 4 (∃𝑤𝑧𝑥𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑤𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
201, 17, 193bitr3i 290 . . 3 (∃𝑥𝑦𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ∃𝑤𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
2120abbii 2736 . 2 {𝑣 ∣ ∃𝑥𝑦𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)} = {𝑣 ∣ ∃𝑤𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))}
22 df-oprab 6619 . 2 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑣 ∣ ∃𝑥𝑦𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
23 df-opab 4684 . 2 {⟨𝑤, 𝑧⟩ ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} = {𝑣 ∣ ∃𝑤𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))}
2421, 22, 233eqtr4i 2653 1 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1480  wex 1701  {cab 2607  cop 4161  {copab 4682  {coprab 6616
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-opab 4684  df-oprab 6619
This theorem is referenced by:  reloprab  6667  oprabv  6668  cbvoprab1  6692  cbvoprab12  6694  cbvoprab3  6696  dmoprab  6706  rnoprab  6708  ssoprab2i  6714  mpt2mptx  6716  resoprab  6721  funoprabg  6724  elrnmpt2res  6739  ov6g  6763  dfoprab3s  7183  xpcomco  8010  omxpenlem  8021  nvss  27336  mpt2mptxf  29361  bj-dfmpt2a  32747  mpt2mptx2  41431
  Copyright terms: Public domain W3C validator