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

Theorem fvopab6 5524
 Description: Value of a function given by ordered-pair class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 11-Sep-2015.)
Hypotheses
Ref Expression
fvopab6.1 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝜑𝑦 = 𝐵)}
fvopab6.2 (𝑥 = 𝐴 → (𝜑𝜓))
fvopab6.3 (𝑥 = 𝐴𝐵 = 𝐶)
Assertion
Ref Expression
fvopab6 ((𝐴𝐷𝐶𝑅𝜓) → (𝐹𝐴) = 𝐶)
Distinct variable groups:   𝑥,𝐴,𝑦   𝜓,𝑥,𝑦   𝑦,𝐵   𝑥,𝐶,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐵(𝑥)   𝐷(𝑥,𝑦)   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem fvopab6
StepHypRef Expression
1 elex 2700 . . 3 (𝐴𝐷𝐴 ∈ V)
2 fvopab6.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
3 fvopab6.3 . . . . . 6 (𝑥 = 𝐴𝐵 = 𝐶)
43eqeq2d 2152 . . . . 5 (𝑥 = 𝐴 → (𝑦 = 𝐵𝑦 = 𝐶))
52, 4anbi12d 465 . . . 4 (𝑥 = 𝐴 → ((𝜑𝑦 = 𝐵) ↔ (𝜓𝑦 = 𝐶)))
6 iba 298 . . . . 5 (𝑦 = 𝐶 → (𝜓 ↔ (𝜓𝑦 = 𝐶)))
76bicomd 140 . . . 4 (𝑦 = 𝐶 → ((𝜓𝑦 = 𝐶) ↔ 𝜓))
8 moeq 2862 . . . . . 6 ∃*𝑦 𝑦 = 𝐵
98moani 2070 . . . . 5 ∃*𝑦(𝜑𝑦 = 𝐵)
109a1i 9 . . . 4 (𝑥 ∈ V → ∃*𝑦(𝜑𝑦 = 𝐵))
11 fvopab6.1 . . . . 5 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝜑𝑦 = 𝐵)}
12 vex 2692 . . . . . . 7 𝑥 ∈ V
1312biantrur 301 . . . . . 6 ((𝜑𝑦 = 𝐵) ↔ (𝑥 ∈ V ∧ (𝜑𝑦 = 𝐵)))
1413opabbii 4002 . . . . 5 {⟨𝑥, 𝑦⟩ ∣ (𝜑𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ (𝜑𝑦 = 𝐵))}
1511, 14eqtri 2161 . . . 4 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ (𝜑𝑦 = 𝐵))}
165, 7, 10, 15fvopab3ig 5502 . . 3 ((𝐴 ∈ V ∧ 𝐶𝑅) → (𝜓 → (𝐹𝐴) = 𝐶))
171, 16sylan 281 . 2 ((𝐴𝐷𝐶𝑅) → (𝜓 → (𝐹𝐴) = 𝐶))
18173impia 1179 1 ((𝐴𝐷𝐶𝑅𝜓) → (𝐹𝐴) = 𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 963   = wceq 1332   ∈ wcel 1481  ∃*wmo 2001  Vcvv 2689  {copab 3995  ‘cfv 5130 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053  ax-pow 4105  ax-pr 4138 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-sbc 2913  df-un 3079  df-in 3081  df-ss 3088  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-br 3937  df-opab 3997  df-id 4222  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-iota 5095  df-fun 5132  df-fv 5138 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator