Theorem opeq2 3826

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
opeq2	⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Proof of Theorem opeq2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2269	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 464	. . . . 5 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		eqidd 2207	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐶} = {𝐶})
4		preq2 3716	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
5	3, 4	preq12d 3723	. . . . . 6 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
6	5	eleq2d 2276	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ {{𝐶}, {𝐶, 𝐴}} ↔ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))
7	2, 6	anbi12d 473	. . . 4 ⊢ (𝐴 = 𝐵 → (((𝐶 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ ((𝐶 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})))
8		df-3an 983	. . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ ((𝐶 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}))
9		df-3an 983	. . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}) ↔ ((𝐶 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))
10	7, 8, 9	3bitr4g 223	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})))
11	10	abbidv 2324	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})} = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})})
12		df-op 3647	. 2 ⊢ ⟨𝐶, 𝐴⟩ = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})}
13		df-op 3647	. 2 ⊢ ⟨𝐶, 𝐵⟩ = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})}
14	11, 12, 13	3eqtr4g 2264	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 981   = wceq 1373   ∈ wcel 2177  {cab 2192  Vcvv 2773  {csn 3638  {cpr 3639  ⟨cop 3641

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647

This theorem is referenced by:  opeq12  3827  opeq2i  3829  opeq2d  3832  oteq2  3835  oteq3  3836  breq2  4055  cbvopab2  4126  cbvopab2v  4129  opthg  4290  eqvinop  4295  opelopabsb  4314  opelxp  4713  opabid2  4817  elrn2g  4876  opeldm  4890  opeldmg  4892  elrn2  4929  opelresg  4975  iss  5014  elimasng  5059  issref  5074  dmsnopg  5163  cnvsng  5177  elxp4  5179  elxp5  5180  dffun5r  5292  funopg  5314  f1osng  5576  tz6.12f  5618  fsn  5765  fsng  5766  fvsng  5793  oveq2  5965  cbvoprab2  6031  ovg  6098  opabex3d  6219  opabex3  6220  op1stg  6249  op2ndg  6250  oprssdmm  6270  op1steq  6278  dfoprab4f  6292  tfrlemibxssdm  6426  tfr1onlembxssdm  6442  tfrcllembxssdm  6455  elixpsn  6835  ixpsnf1o  6836  mapsnen  6917  xpsnen  6931  xpassen  6940  xpf1o  6956  djulclr  7166  djurclr  7167  djulcl  7168  djurcl  7169  djulclb  7172  inl11  7182  djuss  7187  1stinl  7191  2ndinl  7192  1stinr  7193  2ndinr  7194  elreal  7961  ax1rid  8010  fseq1p1m1  10236  pfxval  11150  imasaddfnlemg  13221  cnmpt21  14838  djucllem  15875