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

Theorem fvopab5 7031
Description: The value of a function that is expressed as an ordered pair abstraction. (Contributed by NM, 19-Feb-2006.) (Revised by Mario Carneiro, 11-Sep-2015.)
Hypotheses
Ref Expression
fvopab5.1 𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
fvopab5.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
fvopab5 (𝐴𝑉 → (𝐹𝐴) = (℩𝑦𝜓))
Distinct variable groups:   𝑥,𝑦,𝐴   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)   𝐹(𝑥,𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem fvopab5
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 elex 3493 . 2 (𝐴𝑉𝐴 ∈ V)
2 df-fv 6552 . . . 4 (𝐹𝐴) = (℩𝑧𝐴𝐹𝑧)
3 breq2 5153 . . . . 5 (𝑧 = 𝑦 → (𝐴𝐹𝑧𝐴𝐹𝑦))
4 nfcv 2904 . . . . . 6 𝑦𝐴
5 fvopab5.1 . . . . . . 7 𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
6 nfopab2 5220 . . . . . . 7 𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}
75, 6nfcxfr 2902 . . . . . 6 𝑦𝐹
8 nfcv 2904 . . . . . 6 𝑦𝑧
94, 7, 8nfbr 5196 . . . . 5 𝑦 𝐴𝐹𝑧
10 nfv 1918 . . . . 5 𝑧 𝐴𝐹𝑦
113, 9, 10cbviotaw 6503 . . . 4 (℩𝑧𝐴𝐹𝑧) = (℩𝑦𝐴𝐹𝑦)
122, 11eqtri 2761 . . 3 (𝐹𝐴) = (℩𝑦𝐴𝐹𝑦)
13 nfcv 2904 . . . . . . 7 𝑥𝐴
14 nfopab1 5219 . . . . . . . 8 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}
155, 14nfcxfr 2902 . . . . . . 7 𝑥𝐹
16 nfcv 2904 . . . . . . 7 𝑥𝑦
1713, 15, 16nfbr 5196 . . . . . 6 𝑥 𝐴𝐹𝑦
18 nfv 1918 . . . . . 6 𝑥𝜓
1917, 18nfbi 1907 . . . . 5 𝑥(𝐴𝐹𝑦𝜓)
20 breq1 5152 . . . . . 6 (𝑥 = 𝐴 → (𝑥𝐹𝑦𝐴𝐹𝑦))
21 fvopab5.2 . . . . . 6 (𝑥 = 𝐴 → (𝜑𝜓))
2220, 21bibi12d 346 . . . . 5 (𝑥 = 𝐴 → ((𝑥𝐹𝑦𝜑) ↔ (𝐴𝐹𝑦𝜓)))
23 df-br 5150 . . . . . 6 (𝑥𝐹𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹)
245eleq2i 2826 . . . . . 6 (⟨𝑥, 𝑦⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
25 opabidw 5525 . . . . . 6 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
2623, 24, 253bitri 297 . . . . 5 (𝑥𝐹𝑦𝜑)
2719, 22, 26vtoclg1f 3556 . . . 4 (𝐴 ∈ V → (𝐴𝐹𝑦𝜓))
2827iotabidv 6528 . . 3 (𝐴 ∈ V → (℩𝑦𝐴𝐹𝑦) = (℩𝑦𝜓))
2912, 28eqtrid 2785 . 2 (𝐴 ∈ V → (𝐹𝐴) = (℩𝑦𝜓))
301, 29syl 17 1 (𝐴𝑉 → (𝐹𝐴) = (℩𝑦𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wcel 2107  Vcvv 3475  cop 4635   class class class wbr 5149  {copab 5211  cio 6494  cfv 6544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-iota 6496  df-fv 6552
This theorem is referenced by:  ajval  30114  adjval  31143
  Copyright terms: Public domain W3C validator