Theorem copsex2t 3982

Description: Closed theorem form of copsex2g 3983. (Contributed by NM, 17-Feb-2013.)

Assertion

Ref	Expression
copsex2t	⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))

Distinct variable groups:   𝑥,𝑦,𝜓   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem copsex2t

Step	Hyp	Ref	Expression
1		elisset 2568	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		elisset 2568	. . . 4 ⊢ (𝐵 ∈ 𝑊 → ∃𝑦 𝑦 = 𝐵)
3	1, 2	anim12i 321	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
4		eeanv 1807	. . 3 ⊢ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
5	3, 4	sylibr 137	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵))
6		nfa1 1434	. . . 4 ⊢ Ⅎ𝑥∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))
7		nfe1 1385	. . . . 5 ⊢ Ⅎ𝑥∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
8		nfv 1421	. . . . 5 ⊢ Ⅎ𝑥𝜓
9	7, 8	nfbi 1481	. . . 4 ⊢ Ⅎ𝑥(∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)
10		nfa2 1471	. . . . 5 ⊢ Ⅎ𝑦∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))
11		nfe1 1385	. . . . . . 7 ⊢ Ⅎ𝑦∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11	nfex 1528	. . . . . 6 ⊢ Ⅎ𝑦∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13		nfv 1421	. . . . . 6 ⊢ Ⅎ𝑦𝜓
14	12, 13	nfbi 1481	. . . . 5 ⊢ Ⅎ𝑦(∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)
15		opeq12 3551	. . . . . . . . 9 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
16		copsexg 3981	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
17	16	eqcoms 2043	. . . . . . . . 9 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → (𝜑 ↔ ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
18	15, 17	syl 14	. . . . . . . 8 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
19	18	adantl 262	. . . . . . 7 ⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜑 ↔ ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
20		sp 1401	. . . . . . . . 9 ⊢ (∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) → ∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)))
21	20	19.21bi 1450	. . . . . . . 8 ⊢ (∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)))
22	21	imp 115	. . . . . . 7 ⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜑 ↔ 𝜓))
23	19, 22	bitr3d 179	. . . . . 6 ⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
24	23	ex 108	. . . . 5 ⊢ (∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)))
25	10, 14, 24	exlimd 1488	. . . 4 ⊢ (∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) → (∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)))
26	6, 9, 25	exlimd 1488	. . 3 ⊢ (∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) → (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)))
27	26	imp 115	. 2 ⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ ∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
28	5, 27	sylan2 270	1 ⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98  ∀wal 1241   = wceq 1243  ∃wex 1381   ∈ wcel 1393  ⟨cop 3378

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384

This theorem is referenced by:  opelopabt  3999