Theorem prel12g 4327

Description: Closed form of prel12 4323. (Contributed by AV, 9-Dec-2018.)

Assertion

Ref	Expression
prel12g	⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}))))

Proof of Theorem prel12g

Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2614	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝑦 ↔ 𝐴 = 𝑦))
2	1	notbid 307	. . . . . 6 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 = 𝑦 ↔ ¬ 𝐴 = 𝑦))
3		preq1 4212	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → {𝑥, 𝑦} = {𝐴, 𝑦})
4	3	eqeq1d 2612	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝑦} = {𝑧, 𝐷}))
5		eleq1 2676	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ {𝑧, 𝐷} ↔ 𝐴 ∈ {𝑧, 𝐷}))
6	5	anbi1d 737	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷}) ↔ (𝐴 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷})))
7	4, 6	bibi12d 334	. . . . . 6 ⊢ (𝑥 = 𝐴 → (({𝑥, 𝑦} = {𝑧, 𝐷} ↔ (𝑥 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷})) ↔ ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ (𝐴 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷}))))
8	2, 7	imbi12d 333	. . . . 5 ⊢ (𝑥 = 𝐴 → ((¬ 𝑥 = 𝑦 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ (𝑥 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷}))) ↔ (¬ 𝐴 = 𝑦 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ (𝐴 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷})))))
9	8	imbi2d 329	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝐷 ∈ 𝑌 → (¬ 𝑥 = 𝑦 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ (𝑥 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷})))) ↔ (𝐷 ∈ 𝑌 → (¬ 𝐴 = 𝑦 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ (𝐴 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷}))))))
10		eqeq2 2621	. . . . . . 7 ⊢ (𝑦 = 𝐵 → (𝐴 = 𝑦 ↔ 𝐴 = 𝐵))
11	10	notbid 307	. . . . . 6 ⊢ (𝑦 = 𝐵 → (¬ 𝐴 = 𝑦 ↔ ¬ 𝐴 = 𝐵))
12		preq2 4213	. . . . . . . 8 ⊢ (𝑦 = 𝐵 → {𝐴, 𝑦} = {𝐴, 𝐵})
13	12	eqeq1d 2612	. . . . . . 7 ⊢ (𝑦 = 𝐵 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝑧, 𝐷}))
14		eleq1 2676	. . . . . . . 8 ⊢ (𝑦 = 𝐵 → (𝑦 ∈ {𝑧, 𝐷} ↔ 𝐵 ∈ {𝑧, 𝐷}))
15	14	anbi2d 736	. . . . . . 7 ⊢ (𝑦 = 𝐵 → ((𝐴 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷}) ↔ (𝐴 ∈ {𝑧, 𝐷} ∧ 𝐵 ∈ {𝑧, 𝐷})))
16	13, 15	bibi12d 334	. . . . . 6 ⊢ (𝑦 = 𝐵 → (({𝐴, 𝑦} = {𝑧, 𝐷} ↔ (𝐴 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷})) ↔ ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ (𝐴 ∈ {𝑧, 𝐷} ∧ 𝐵 ∈ {𝑧, 𝐷}))))
17	11, 16	imbi12d 333	. . . . 5 ⊢ (𝑦 = 𝐵 → ((¬ 𝐴 = 𝑦 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ (𝐴 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷}))) ↔ (¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ (𝐴 ∈ {𝑧, 𝐷} ∧ 𝐵 ∈ {𝑧, 𝐷})))))
18	17	imbi2d 329	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝐷 ∈ 𝑌 → (¬ 𝐴 = 𝑦 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ (𝐴 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷})))) ↔ (𝐷 ∈ 𝑌 → (¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ (𝐴 ∈ {𝑧, 𝐷} ∧ 𝐵 ∈ {𝑧, 𝐷}))))))
19		preq1 4212	. . . . . . . 8 ⊢ (𝑧 = 𝐶 → {𝑧, 𝐷} = {𝐶, 𝐷})
20	19	eqeq2d 2620	. . . . . . 7 ⊢ (𝑧 = 𝐶 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝐶, 𝐷}))
21	19	eleq2d 2673	. . . . . . . 8 ⊢ (𝑧 = 𝐶 → (𝐴 ∈ {𝑧, 𝐷} ↔ 𝐴 ∈ {𝐶, 𝐷}))
22	19	eleq2d 2673	. . . . . . . 8 ⊢ (𝑧 = 𝐶 → (𝐵 ∈ {𝑧, 𝐷} ↔ 𝐵 ∈ {𝐶, 𝐷}))
23	21, 22	anbi12d 743	. . . . . . 7 ⊢ (𝑧 = 𝐶 → ((𝐴 ∈ {𝑧, 𝐷} ∧ 𝐵 ∈ {𝑧, 𝐷}) ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})))
24	20, 23	bibi12d 334	. . . . . 6 ⊢ (𝑧 = 𝐶 → (({𝐴, 𝐵} = {𝑧, 𝐷} ↔ (𝐴 ∈ {𝑧, 𝐷} ∧ 𝐵 ∈ {𝑧, 𝐷})) ↔ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}))))
25	24	imbi2d 329	. . . . 5 ⊢ (𝑧 = 𝐶 → ((¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ (𝐴 ∈ {𝑧, 𝐷} ∧ 𝐵 ∈ {𝑧, 𝐷}))) ↔ (¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})))))
26	25	imbi2d 329	. . . 4 ⊢ (𝑧 = 𝐶 → ((𝐷 ∈ 𝑌 → (¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ (𝐴 ∈ {𝑧, 𝐷} ∧ 𝐵 ∈ {𝑧, 𝐷})))) ↔ (𝐷 ∈ 𝑌 → (¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}))))))
27		preq2 4213	. . . . . . . . 9 ⊢ (𝑤 = 𝐷 → {𝑧, 𝑤} = {𝑧, 𝐷})
28	27	eqeq2d 2620	. . . . . . . 8 ⊢ (𝑤 = 𝐷 → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ {𝑥, 𝑦} = {𝑧, 𝐷}))
29	27	eleq2d 2673	. . . . . . . . 9 ⊢ (𝑤 = 𝐷 → (𝑥 ∈ {𝑧, 𝑤} ↔ 𝑥 ∈ {𝑧, 𝐷}))
30	27	eleq2d 2673	. . . . . . . . 9 ⊢ (𝑤 = 𝐷 → (𝑦 ∈ {𝑧, 𝑤} ↔ 𝑦 ∈ {𝑧, 𝐷}))
31	29, 30	anbi12d 743	. . . . . . . 8 ⊢ (𝑤 = 𝐷 → ((𝑥 ∈ {𝑧, 𝑤} ∧ 𝑦 ∈ {𝑧, 𝑤}) ↔ (𝑥 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷})))
32	28, 31	bibi12d 334	. . . . . . 7 ⊢ (𝑤 = 𝐷 → (({𝑥, 𝑦} = {𝑧, 𝑤} ↔ (𝑥 ∈ {𝑧, 𝑤} ∧ 𝑦 ∈ {𝑧, 𝑤})) ↔ ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ (𝑥 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷}))))
33	32	imbi2d 329	. . . . . 6 ⊢ (𝑤 = 𝐷 → ((¬ 𝑥 = 𝑦 → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ (𝑥 ∈ {𝑧, 𝑤} ∧ 𝑦 ∈ {𝑧, 𝑤}))) ↔ (¬ 𝑥 = 𝑦 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ (𝑥 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷})))))
34		vex 3176	. . . . . . 7 ⊢ 𝑥 ∈ V
35		vex 3176	. . . . . . 7 ⊢ 𝑦 ∈ V
36		vex 3176	. . . . . . 7 ⊢ 𝑧 ∈ V
37		vex 3176	. . . . . . 7 ⊢ 𝑤 ∈ V
38	34, 35, 36, 37	prel12 4323	. . . . . 6 ⊢ (¬ 𝑥 = 𝑦 → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ (𝑥 ∈ {𝑧, 𝑤} ∧ 𝑦 ∈ {𝑧, 𝑤})))
39	33, 38	vtoclg 3239	. . . . 5 ⊢ (𝐷 ∈ 𝑌 → (¬ 𝑥 = 𝑦 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ (𝑥 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷}))))
40	39	a1i 11	. . . 4 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑋) → (𝐷 ∈ 𝑌 → (¬ 𝑥 = 𝑦 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ (𝑥 ∈ {𝑧, 𝐷} ∧ 𝑦 ∈ {𝑧, 𝐷})))))
41	9, 18, 26, 40	vtocl3ga 3249	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ 𝑌 → (¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})))))
42	41	3expa 1257	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ 𝑌 → (¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})))))
43	42	impr 647	1 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128

This theorem is referenced by:  hash2prd  13114