Theorem cgsex4g 3538

Description: An implicit substitution inference for 4 general classes. (Contributed by NM, 5-Aug-1995.) Avoid ax-10 2139. (Revised by Gino Giotto, 20-Aug-2023.)

Hypotheses

Ref	Expression
cgsex4g.1	⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → 𝜒)
cgsex4g.2	⊢ (𝜒 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cgsex4g	⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) ↔ 𝜓))

Distinct variable groups:   𝑥,𝑦,𝑧,𝑤,𝐴   𝑥,𝐵,𝑦,𝑧,𝑤   𝑥,𝐶,𝑦,𝑧,𝑤   𝑥,𝐷,𝑦,𝑧,𝑤   𝜓,𝑥,𝑦,𝑧,𝑤

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤)   𝜒(𝑥,𝑦,𝑧,𝑤)   𝑅(𝑥,𝑦,𝑧,𝑤)   𝑆(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem cgsex4g

Step	Hyp	Ref	Expression
1		cgsex4g.2	. . . . 5 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
2	1	biimpa 479	. . . 4 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	exlimivv 1927	. . 3 ⊢ (∃𝑧∃𝑤(𝜒 ∧ 𝜑) → 𝜓)
4	3	exlimivv 1927	. 2 ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) → 𝜓)
5		elisset 3504	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑅 → ∃𝑥 𝑥 = 𝐴)
6		elisset 3504	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑆 → ∃𝑦 𝑦 = 𝐵)
7	5, 6	anim12i 614	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
8		exdistrv 1950	. . . . . . 7 ⊢ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
9	7, 8	sylibr 236	. . . . . 6 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵))
10		elisset 3504	. . . . . . . 8 ⊢ (𝐶 ∈ 𝑅 → ∃𝑧 𝑧 = 𝐶)
11		elisset 3504	. . . . . . . 8 ⊢ (𝐷 ∈ 𝑆 → ∃𝑤 𝑤 = 𝐷)
12	10, 11	anim12i 614	. . . . . . 7 ⊢ ((𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆) → (∃𝑧 𝑧 = 𝐶 ∧ ∃𝑤 𝑤 = 𝐷))
13		exdistrv 1950	. . . . . . 7 ⊢ (∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷) ↔ (∃𝑧 𝑧 = 𝐶 ∧ ∃𝑤 𝑤 = 𝐷))
14	12, 13	sylibr 236	. . . . . 6 ⊢ ((𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆) → ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷))
15	9, 14	anim12i 614	. . . . 5 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷)))
16		excom 2162	. . . . . . 7 ⊢ (∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ∃𝑧∃𝑦∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)))
17	16	exbii 1842	. . . . . 6 ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ∃𝑥∃𝑧∃𝑦∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)))
18		4exdistrv 1951	. . . . . 6 ⊢ (∃𝑥∃𝑧∃𝑦∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷)))
19	17, 18	bitri 277	. . . . 5 ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷)))
20	15, 19	sylibr 236	. . . 4 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → ∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)))
21		cgsex4g.1	. . . . . 6 ⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → 𝜒)
22	21	2eximi 1830	. . . . 5 ⊢ (∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → ∃𝑧∃𝑤𝜒)
23	22	2eximi 1830	. . . 4 ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → ∃𝑥∃𝑦∃𝑧∃𝑤𝜒)
24	20, 23	syl 17	. . 3 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → ∃𝑥∃𝑦∃𝑧∃𝑤𝜒)
25	1	biimprcd 252	. . . . . 6 ⊢ (𝜓 → (𝜒 → 𝜑))
26	25	ancld 553	. . . . 5 ⊢ (𝜓 → (𝜒 → (𝜒 ∧ 𝜑)))
27	26	2eximdv 1914	. . . 4 ⊢ (𝜓 → (∃𝑧∃𝑤𝜒 → ∃𝑧∃𝑤(𝜒 ∧ 𝜑)))
28	27	2eximdv 1914	. . 3 ⊢ (𝜓 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜒 → ∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑)))
29	24, 28	syl5com 31	. 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (𝜓 → ∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑)))
30	4, 29	impbid2 228	1 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1531  ∃wex 1774   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-11 2154  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-cleq 2812  df-clel 2891

This theorem is referenced by:  copsex4g  5376  brecop  8382