Theorem cgsex2gd

Description: Implicit substitution inference for general classes. (Contributed by NM, 26-Jul-1995) Adapt cgsex2g to deduction form. (Revised by BJ, 28-Mar-2026) Do not use cgsex2g . (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	cgsex2gd.is	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝜓 )
	cgsex2gd.maj	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 ↔ 𝜃 ) )
Assertion	cgsex2gd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝜓 ∧ 𝜒 ) ↔ 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		cgsex2gd.is	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝜓 )
2		cgsex2gd.maj	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 ↔ 𝜃 ) )
3	2	biimp3a	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
4	3	3expib	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) → 𝜃 ) )
5	4	exlimdvv	⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ( 𝜓 ∧ 𝜒 ) → 𝜃 ) )
6	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝜓 ∧ 𝜒 ) → 𝜃 ) )
7	1	ex	⊢ ( 𝜑 → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝜓 ) )
8	7	2eximdv	⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ∃ 𝑥 ∃ 𝑦 𝜓 ) )
9		elisset	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 )
10		elisset	⊢ ( 𝐵 ∈ 𝑊 → ∃ 𝑦 𝑦 = 𝐵 )
11	9 10	anim12i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑥 𝑥 = 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) )
12		exdistrv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) )
13	11 12	sylibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
14	8 13	impel	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ∃ 𝑥 ∃ 𝑦 𝜓 )
15	2	biimprd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜃 → 𝜒 ) )
16	15	impancom	⊢ ( ( 𝜑 ∧ 𝜃 ) → ( 𝜓 → 𝜒 ) )
17	16	ancld	⊢ ( ( 𝜑 ∧ 𝜃 ) → ( 𝜓 → ( 𝜓 ∧ 𝜒 ) ) )
18	17	2eximdv	⊢ ( ( 𝜑 ∧ 𝜃 ) → ( ∃ 𝑥 ∃ 𝑦 𝜓 → ∃ 𝑥 ∃ 𝑦 ( 𝜓 ∧ 𝜒 ) ) )
19	18	expimpd	⊢ ( 𝜑 → ( ( 𝜃 ∧ ∃ 𝑥 ∃ 𝑦 𝜓 ) → ∃ 𝑥 ∃ 𝑦 ( 𝜓 ∧ 𝜒 ) ) )
20	19	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ( 𝜃 ∧ ∃ 𝑥 ∃ 𝑦 𝜓 ) → ∃ 𝑥 ∃ 𝑦 ( 𝜓 ∧ 𝜒 ) ) )
21	14 20	mpan2d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( 𝜃 → ∃ 𝑥 ∃ 𝑦 ( 𝜓 ∧ 𝜒 ) ) )
22	6 21	impbid	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝜓 ∧ 𝜒 ) ↔ 𝜃 ) )