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

Theorem opeq1 3705
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 2202 . . . . . 6 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi1d 460 . . . . 5 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3 sneq 3538 . . . . . . 7 (𝐴 = 𝐵 → {𝐴} = {𝐵})
4 preq1 3600 . . . . . . 7 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
53, 4preq12d 3608 . . . . . 6 (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
65eleq2d 2209 . . . . 5 (𝐴 = 𝐵 → (𝑥 ∈ {{𝐴}, {𝐴, 𝐶}} ↔ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
72, 6anbi12d 464 . . . 4 (𝐴 = 𝐵 → (((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
8 df-3an 964 . . . 4 ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}))
9 df-3an 964 . . . 4 ((𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
107, 8, 93bitr4g 222 . . 3 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
1110abbidv 2257 . 2 (𝐴 = 𝐵 → {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})} = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})})
12 df-op 3536 . 2 𝐴, 𝐶⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})}
13 df-op 3536 . 2 𝐵, 𝐶⟩ = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})}
1411, 12, 133eqtr4g 2197 1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 962   = wceq 1331  wcel 1480  {cab 2125  Vcvv 2686  {csn 3527  {cpr 3528  cop 3530
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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536
This theorem is referenced by:  opeq12  3707  opeq1i  3708  opeq1d  3711  oteq1  3714  breq1  3932  cbvopab1  4001  cbvopab1s  4003  opthg  4160  eqvinop  4165  opelopabsb  4182  opelxp  4569  elvvv  4602  opabid2  4670  opeliunxp2  4679  elsnres  4856  elimasng  4907  rnxpid  4973  dmsnopg  5010  cnvsng  5024  elxp4  5026  elxp5  5027  funopg  5157  f1osng  5408  dmfco  5489  fvelrn  5551  fsng  5593  fvsng  5616  funfvima3  5651  oveq1  5781  oprabid  5803  dfoprab2  5818  cbvoprab1  5843  opabex3d  6019  opabex3  6020  op1stg  6048  op2ndg  6049  oprssdmm  6069  dfoprab4f  6091  cnvoprab  6131  opeliunxp2f  6135  tfr1onlemaccex  6245  tfrcllemaccex  6258  elixpsn  6629  fundmen  6700  xpsnen  6715  xpassen  6724  xpf1o  6738  ltexnqq  7230  archnqq  7239  prarloclemarch2  7241  prarloclemlo  7316  prarloclem3  7319  prarloclem5  7322  caucvgprlemnkj  7488  caucvgprlemnbj  7489  caucvgprlemm  7490  caucvgprlemdisj  7496  caucvgprlemloc  7497  caucvgprlemcl  7498  caucvgprlemladdfu  7499  caucvgprlemladdrl  7500  caucvgprlem1  7501  caucvgprlem2  7502  caucvgpr  7504  caucvgprprlemell  7507  caucvgprprlemelu  7508  caucvgprprlemcbv  7509  caucvgprprlemval  7510  caucvgprprlemnkeqj  7512  caucvgprprlemmu  7517  caucvgprprlemopl  7519  caucvgprprlemlol  7520  caucvgprprlemopu  7521  caucvgprprlemloc  7525  caucvgprprlemclphr  7527  caucvgprprlemexbt  7528  caucvgprprlem1  7531  caucvgprprlem2  7532  caucvgsr  7624  suplocsrlemb  7628  suplocsrlempr  7629  suplocsrlem  7630  suplocsr  7631  elrealeu  7651  pitonn  7670  nntopi  7716  axcaucvglemval  7719  axcaucvg  7722  axpre-suploclemres  7723  fsum2dlemstep  11217  cnmpt21  12476
  Copyright terms: Public domain W3C validator