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

Theorem opeq1 3546
Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opeq1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Proof of Theorem opeq1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eleq1 2100 . . . . . 6 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi1d 438 . . . . 5 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3 sneq 3383 . . . . . . 7 (𝐴 = 𝐵 → {𝐴} = {𝐵})
4 preq1 3444 . . . . . . 7 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
53, 4preq12d 3452 . . . . . 6 (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
65eleq2d 2107 . . . . 5 (𝐴 = 𝐵 → (𝑥 ∈ {{𝐴}, {𝐴, 𝐶}} ↔ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
72, 6anbi12d 442 . . . 4 (𝐴 = 𝐵 → (((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
8 df-3an 887 . . . 4 ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}))
9 df-3an 887 . . . 4 ((𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
107, 8, 93bitr4g 212 . . 3 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
1110abbidv 2155 . 2 (𝐴 = 𝐵 → {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})} = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})})
12 df-op 3381 . 2 𝐴, 𝐶⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})}
13 df-op 3381 . 2 𝐵, 𝐶⟩ = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})}
1411, 12, 133eqtr4g 2097 1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  w3a 885   = wceq 1243  wcel 1393  {cab 2026  Vcvv 2554  {csn 3372  {cpr 3373  cop 3375
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2556  df-un 2919  df-sn 3378  df-pr 3379  df-op 3381
This theorem is referenced by:  opeq12  3548  opeq1i  3549  opeq1d  3552  oteq1  3555  breq1  3764  cbvopab1  3827  cbvopab1s  3829  opthg  3972  eqvinop  3977  opelopabsb  3994  opelxp  4361  elvvv  4390  opabid2  4454  opeliunxp2  4463  elsnres  4634  elimasng  4680  rnxpid  4742  dmsnopg  4779  cnvsng  4793  elxp4  4795  elxp5  4796  funopg  4921  f1osng  5154  dmfco  5228  fvelrn  5285  fsng  5323  fvsng  5346  funfvima3  5379  oveq1  5506  oprabid  5524  dfoprab2  5539  cbvoprab1  5563  opabex3d  5735  opabex3  5736  op1stg  5764  op2ndg  5765  dfoprab4f  5806  fundmen  6273  xpsnen  6282  xpassen  6291  ltexnqq  6487  archnqq  6496  prarloclemarch2  6498  prarloclemlo  6573  prarloclem3  6576  prarloclem5  6579  caucvgprlemnkj  6745  caucvgprlemnbj  6746  caucvgprlemm  6747  caucvgprlemdisj  6753  caucvgprlemloc  6754  caucvgprlemcl  6755  caucvgprlemladdfu  6756  caucvgprlemladdrl  6757  caucvgprlem1  6758  caucvgprlem2  6759  caucvgpr  6761  caucvgprprlemell  6764  caucvgprprlemelu  6765  caucvgprprlemcbv  6766  caucvgprprlemval  6767  caucvgprprlemnkeqj  6769  caucvgprprlemmu  6774  caucvgprprlemopl  6776  caucvgprprlemlol  6777  caucvgprprlemopu  6778  caucvgprprlemloc  6782  caucvgprprlemclphr  6784  caucvgprprlemexbt  6785  caucvgprprlem1  6788  caucvgprprlem2  6789  caucvgsr  6867  elrealeu  6887  pitonn  6905  nntopi  6949  axcaucvglemval  6952  axcaucvg  6955
  Copyright terms: Public domain W3C validator