Theorem opeq1 3793

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.

Step	Hyp	Ref	Expression
1		eleq1 2252	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 465	. . . . 5 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 3618	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 3684	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 3692	. . . . . 6 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	5	eleq2d 2259	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ {{𝐴}, {𝐴, 𝐶}} ↔ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
7	2, 6	anbi12d 473	. . . 4 ⊢ (𝐴 = 𝐵 → (((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
8		df-3an 982	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}))
9		df-3an 982	. . . 4 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
10	7, 8, 9	3bitr4g 223	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
11	10	abbidv 2307	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})} = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})})
12		df-op 3616	. 2 ⊢ ⟨𝐴, 𝐶⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})}
13		df-op 3616	. 2 ⊢ ⟨𝐵, 𝐶⟩ = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})}
14	11, 12, 13	3eqtr4g 2247	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980   = wceq 1364   ∈ wcel 2160  {cab 2175  Vcvv 2752  {csn 3607  {cpr 3608  ⟨cop 3610

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616

This theorem is referenced by:  opeq12  3795  opeq1i  3796  opeq1d  3799  oteq1  3802  breq1  4021  cbvopab1  4091  cbvopab1s  4093  opthg  4256  eqvinop  4261  opelopabsb  4278  opelxp  4674  elvvv  4707  opabid2  4776  opeliunxp2  4785  elsnres  4962  elimasng  5014  rnxpid  5081  dmsnopg  5118  cnvsng  5132  elxp4  5134  elxp5  5135  funopg  5269  f1osng  5521  dmfco  5605  fvelrn  5668  fsng  5710  fvsng  5733  funfvima3  5771  oveq1  5904  oprabid  5929  dfoprab2  5944  cbvoprab1  5969  opabex3d  6147  opabex3  6148  op1stg  6176  op2ndg  6177  oprssdmm  6197  dfoprab4f  6219  cnvoprab  6260  opeliunxp2f  6264  tfr1onlemaccex  6374  tfrcllemaccex  6387  elixpsn  6762  fundmen  6833  xpsnen  6848  xpassen  6857  xpf1o  6873  ltexnqq  7438  archnqq  7447  prarloclemarch2  7449  prarloclemlo  7524  prarloclem3  7527  prarloclem5  7530  caucvgprlemnkj  7696  caucvgprlemnbj  7697  caucvgprlemm  7698  caucvgprlemdisj  7704  caucvgprlemloc  7705  caucvgprlemcl  7706  caucvgprlemladdfu  7707  caucvgprlemladdrl  7708  caucvgprlem1  7709  caucvgprlem2  7710  caucvgpr  7712  caucvgprprlemell  7715  caucvgprprlemelu  7716  caucvgprprlemcbv  7717  caucvgprprlemval  7718  caucvgprprlemnkeqj  7720  caucvgprprlemmu  7725  caucvgprprlemopl  7727  caucvgprprlemlol  7728  caucvgprprlemopu  7729  caucvgprprlemloc  7733  caucvgprprlemclphr  7735  caucvgprprlemexbt  7736  caucvgprprlem1  7739  caucvgprprlem2  7740  caucvgsr  7832  suplocsrlemb  7836  suplocsrlempr  7837  suplocsrlem  7838  suplocsr  7839  elrealeu  7859  pitonn  7878  nntopi  7924  axcaucvglemval  7927  axcaucvg  7930  axpre-suploclemres  7931  fsum2dlemstep  11477  fprod2dlemstep  11665  imasaddfnlemg  12794  cnmpt21  14268