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

Theorem f1veqaeq 5769
Description: If the values of a one-to-one function for two arguments are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
Assertion
Ref Expression
f1veqaeq ((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) → ((𝐹𝐶) = (𝐹𝐷) → 𝐶 = 𝐷))

Proof of Theorem f1veqaeq
Dummy variables 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dff13 5768 . . 3 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑐𝐴𝑑𝐴 ((𝐹𝑐) = (𝐹𝑑) → 𝑐 = 𝑑)))
2 fveq2 5515 . . . . . . . 8 (𝑐 = 𝐶 → (𝐹𝑐) = (𝐹𝐶))
32eqeq1d 2186 . . . . . . 7 (𝑐 = 𝐶 → ((𝐹𝑐) = (𝐹𝑑) ↔ (𝐹𝐶) = (𝐹𝑑)))
4 eqeq1 2184 . . . . . . 7 (𝑐 = 𝐶 → (𝑐 = 𝑑𝐶 = 𝑑))
53, 4imbi12d 234 . . . . . 6 (𝑐 = 𝐶 → (((𝐹𝑐) = (𝐹𝑑) → 𝑐 = 𝑑) ↔ ((𝐹𝐶) = (𝐹𝑑) → 𝐶 = 𝑑)))
6 fveq2 5515 . . . . . . . 8 (𝑑 = 𝐷 → (𝐹𝑑) = (𝐹𝐷))
76eqeq2d 2189 . . . . . . 7 (𝑑 = 𝐷 → ((𝐹𝐶) = (𝐹𝑑) ↔ (𝐹𝐶) = (𝐹𝐷)))
8 eqeq2 2187 . . . . . . 7 (𝑑 = 𝐷 → (𝐶 = 𝑑𝐶 = 𝐷))
97, 8imbi12d 234 . . . . . 6 (𝑑 = 𝐷 → (((𝐹𝐶) = (𝐹𝑑) → 𝐶 = 𝑑) ↔ ((𝐹𝐶) = (𝐹𝐷) → 𝐶 = 𝐷)))
105, 9rspc2v 2854 . . . . 5 ((𝐶𝐴𝐷𝐴) → (∀𝑐𝐴𝑑𝐴 ((𝐹𝑐) = (𝐹𝑑) → 𝑐 = 𝑑) → ((𝐹𝐶) = (𝐹𝐷) → 𝐶 = 𝐷)))
1110com12 30 . . . 4 (∀𝑐𝐴𝑑𝐴 ((𝐹𝑐) = (𝐹𝑑) → 𝑐 = 𝑑) → ((𝐶𝐴𝐷𝐴) → ((𝐹𝐶) = (𝐹𝐷) → 𝐶 = 𝐷)))
1211adantl 277 . . 3 ((𝐹:𝐴𝐵 ∧ ∀𝑐𝐴𝑑𝐴 ((𝐹𝑐) = (𝐹𝑑) → 𝑐 = 𝑑)) → ((𝐶𝐴𝐷𝐴) → ((𝐹𝐶) = (𝐹𝐷) → 𝐶 = 𝐷)))
131, 12sylbi 121 . 2 (𝐹:𝐴1-1𝐵 → ((𝐶𝐴𝐷𝐴) → ((𝐹𝐶) = (𝐹𝐷) → 𝐶 = 𝐷)))
1413imp 124 1 ((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) → ((𝐹𝐶) = (𝐹𝐷) → 𝐶 = 𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104   = wceq 1353  wcel 2148  wral 2455  wf 5212  1-1wf1 5213  cfv 5216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-sbc 2963  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-opab 4065  df-id 4293  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fv 5224
This theorem is referenced by:  f1fveq  5772  f1ocnvfvrneq  5782  f1o2ndf1  6228  fidceq  6868  difinfsnlem  7097  difinfsn  7098  iseqf1olemab  10488  iseqf1olemnanb  10489  pwle2  14684
  Copyright terms: Public domain W3C validator