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

Theorem opeq1 3675
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 2180 . . . . . 6 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi1d 460 . . . . 5 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3 sneq 3508 . . . . . . 7 (𝐴 = 𝐵 → {𝐴} = {𝐵})
4 preq1 3570 . . . . . . 7 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
53, 4preq12d 3578 . . . . . 6 (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
65eleq2d 2187 . . . . 5 (𝐴 = 𝐵 → (𝑥 ∈ {{𝐴}, {𝐴, 𝐶}} ↔ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
72, 6anbi12d 464 . . . 4 (𝐴 = 𝐵 → (((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
8 df-3an 949 . . . 4 ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}))
9 df-3an 949 . . . 4 ((𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
107, 8, 93bitr4g 222 . . 3 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
1110abbidv 2235 . 2 (𝐴 = 𝐵 → {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})} = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})})
12 df-op 3506 . 2 𝐴, 𝐶⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})}
13 df-op 3506 . 2 𝐵, 𝐶⟩ = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})}
1411, 12, 133eqtr4g 2175 1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 947   = wceq 1316  wcel 1465  {cab 2103  Vcvv 2660  {csn 3497  {cpr 3498  cop 3500
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506
This theorem is referenced by:  opeq12  3677  opeq1i  3678  opeq1d  3681  oteq1  3684  breq1  3902  cbvopab1  3971  cbvopab1s  3973  opthg  4130  eqvinop  4135  opelopabsb  4152  opelxp  4539  elvvv  4572  opabid2  4640  opeliunxp2  4649  elsnres  4826  elimasng  4877  rnxpid  4943  dmsnopg  4980  cnvsng  4994  elxp4  4996  elxp5  4997  funopg  5127  f1osng  5376  dmfco  5457  fvelrn  5519  fsng  5561  fvsng  5584  funfvima3  5619  oveq1  5749  oprabid  5771  dfoprab2  5786  cbvoprab1  5811  opabex3d  5987  opabex3  5988  op1stg  6016  op2ndg  6017  oprssdmm  6037  dfoprab4f  6059  cnvoprab  6099  opeliunxp2f  6103  tfr1onlemaccex  6213  tfrcllemaccex  6226  elixpsn  6597  fundmen  6668  xpsnen  6683  xpassen  6692  xpf1o  6706  ltexnqq  7184  archnqq  7193  prarloclemarch2  7195  prarloclemlo  7270  prarloclem3  7273  prarloclem5  7276  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemm  7444  caucvgprlemdisj  7450  caucvgprlemloc  7451  caucvgprlemcl  7452  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  caucvgprlem1  7455  caucvgprlem2  7456  caucvgpr  7458  caucvgprprlemell  7461  caucvgprprlemelu  7462  caucvgprprlemcbv  7463  caucvgprprlemval  7464  caucvgprprlemnkeqj  7466  caucvgprprlemmu  7471  caucvgprprlemopl  7473  caucvgprprlemlol  7474  caucvgprprlemopu  7475  caucvgprprlemloc  7479  caucvgprprlemclphr  7481  caucvgprprlemexbt  7482  caucvgprprlem1  7485  caucvgprprlem2  7486  caucvgsr  7578  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  suplocsr  7585  elrealeu  7605  pitonn  7624  nntopi  7670  axcaucvglemval  7673  axcaucvg  7676  axpre-suploclemres  7677  fsum2dlemstep  11158  cnmpt21  12371
  Copyright terms: Public domain W3C validator