Theorem opeq1 3818

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 2267	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 465	. . . . 5 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 3643	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 3709	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 3717	. . . . . 6 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	5	eleq2d 2274	. . . . 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 2322	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})} = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})})
12		df-op 3641	. 2 ⊢ ⟨𝐴, 𝐶⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})}
13		df-op 3641	. 2 ⊢ ⟨𝐵, 𝐶⟩ = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})}
14	11, 12, 13	3eqtr4g 2262	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980   = wceq 1372   ∈ wcel 2175  {cab 2190  Vcvv 2771  {csn 3632  {cpr 3633  ⟨cop 3635

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641

This theorem is referenced by:  opeq12  3820  opeq1i  3821  opeq1d  3824  oteq1  3827  breq1  4046  cbvopab1  4116  cbvopab1s  4118  opthg  4281  eqvinop  4286  opelopabsb  4305  opelxp  4704  elvvv  4737  opabid2  4808  opeliunxp2  4817  elsnres  4995  elimasng  5049  rnxpid  5116  dmsnopg  5153  cnvsng  5167  elxp4  5169  elxp5  5170  funopg  5304  f1osng  5562  dmfco  5646  fvelrn  5710  fsng  5752  fvsng  5779  funfvima3  5817  oveq1  5950  oprabid  5975  dfoprab2  5991  cbvoprab1  6016  opabex3d  6205  opabex3  6206  op1stg  6235  op2ndg  6236  oprssdmm  6256  dfoprab4f  6278  cnvoprab  6319  opeliunxp2f  6323  tfr1onlemaccex  6433  tfrcllemaccex  6446  elixpsn  6821  fundmen  6897  xpsnen  6915  xpassen  6924  xpf1o  6940  ltexnqq  7520  archnqq  7529  prarloclemarch2  7531  prarloclemlo  7606  prarloclem3  7609  prarloclem5  7612  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemm  7780  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprlemcl  7788  caucvgprlemladdfu  7789  caucvgprlemladdrl  7790  caucvgprlem1  7791  caucvgprlem2  7792  caucvgpr  7794  caucvgprprlemell  7797  caucvgprprlemelu  7798  caucvgprprlemcbv  7799  caucvgprprlemval  7800  caucvgprprlemnkeqj  7802  caucvgprprlemmu  7807  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemopu  7811  caucvgprprlemloc  7815  caucvgprprlemclphr  7817  caucvgprprlemexbt  7818  caucvgprprlem1  7821  caucvgprprlem2  7822  caucvgsr  7914  suplocsrlemb  7918  suplocsrlempr  7919  suplocsrlem  7920  suplocsr  7921  elrealeu  7941  pitonn  7960  nntopi  8006  axcaucvglemval  8009  axcaucvg  8012  axpre-suploclemres  8013  fsum2dlemstep  11687  fprod2dlemstep  11875  imasaddfnlemg  13088  cnmpt21  14705