riotasv3d

Description: A property ch holding for a representative of a single-valued class expression C ( y ) (see e.g. reusv2 ) also holds for its description binder D (in the form of property th ). (Contributed by NM, 5-Mar-2013) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	riotasv3d.1	⊢ Ⅎ 𝑦 𝜑
	riotasv3d.2	⊢ ( 𝜑 → Ⅎ 𝑦 𝜃 )
	riotasv3d.3	⊢ ( 𝜑 → 𝐷 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) )
	riotasv3d.4	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐷 ) → ( 𝜒 ↔ 𝜃 ) )
	riotasv3d.5	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) → 𝜒 ) )
	riotasv3d.6	⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
	riotasv3d.7	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐵 𝜓 )
Assertion	riotasv3d	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		riotasv3d.1	⊢ Ⅎ 𝑦 𝜑
2		riotasv3d.2	⊢ ( 𝜑 → Ⅎ 𝑦 𝜃 )
3		riotasv3d.3	⊢ ( 𝜑 → 𝐷 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) )
4		riotasv3d.4	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐷 ) → ( 𝜒 ↔ 𝜃 ) )
5		riotasv3d.5	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) → 𝜒 ) )
6		riotasv3d.6	⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
7		riotasv3d.7	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐵 𝜓 )
8		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
9	7	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ V ) → ∃ 𝑦 ∈ 𝐵 𝜓 )
10		nfv	⊢ Ⅎ 𝑦 𝐴 ∈ V
11	5	imp	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) → 𝜒 )
12	11	adantrl	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) ) → 𝜒 )
13	3 6	riotasvd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ V ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) → 𝐷 = 𝐶 ) )
14	13	impr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) ) → 𝐷 = 𝐶 )
15	14	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) ) → 𝐶 = 𝐷 )
16	15 4	syldan	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) ) → ( 𝜒 ↔ 𝜃 ) )
17	12 16	mpbid	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) ) → 𝜃 )
18	17	exp45	⊢ ( 𝜑 → ( 𝐴 ∈ V → ( 𝑦 ∈ 𝐵 → ( 𝜓 → 𝜃 ) ) ) )
19	1 10 18	ralrimd	⊢ ( 𝜑 → ( 𝐴 ∈ V → ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝜃 ) ) )
20		r19.23t	⊢ ( Ⅎ 𝑦 𝜃 → ( ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝜃 ) ↔ ( ∃ 𝑦 ∈ 𝐵 𝜓 → 𝜃 ) ) )
21	2 20	syl	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝜃 ) ↔ ( ∃ 𝑦 ∈ 𝐵 𝜓 → 𝜃 ) ) )
22	19 21	sylibd	⊢ ( 𝜑 → ( 𝐴 ∈ V → ( ∃ 𝑦 ∈ 𝐵 𝜓 → 𝜃 ) ) )
23	22	imp	⊢ ( ( 𝜑 ∧ 𝐴 ∈ V ) → ( ∃ 𝑦 ∈ 𝐵 𝜓 → 𝜃 ) )
24	9 23	mpd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ V ) → 𝜃 )
25	8 24	sylan2	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → 𝜃 )

Metamath Proof Explorer

Theorem riotasv3d

Proof