riota2df

Description: A deduction version of riota2f . (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	riota2df.1	⊢ Ⅎ 𝑥 𝜑
	riota2df.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
	riota2df.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
	riota2df.4	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
	riota2df.5	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	riota2df	⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ( 𝜒 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		riota2df.1	⊢ Ⅎ 𝑥 𝜑
2		riota2df.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
3		riota2df.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
4		riota2df.4	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
5		riota2df.5	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
6	4	adantr	⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → 𝐵 ∈ 𝐴 )
7		simpr	⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ∃! 𝑥 ∈ 𝐴 𝜓 )
8		df-reu	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜓 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
9	7 8	sylib	⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
10		simpr	⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 )
11	6	adantr	⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → 𝐵 ∈ 𝐴 )
12	10 11	eqeltrd	⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ 𝐴 )
13	12	biantrurd	⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → ( 𝜓 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
14	5	adantlr	⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
15	13 14	bitr3d	⊢ ( ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 = 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ 𝜒 ) )
16		nfreu1	⊢ Ⅎ 𝑥 ∃! 𝑥 ∈ 𝐴 𝜓
17	1 16	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 )
18	3	adantr	⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → Ⅎ 𝑥 𝜒 )
19	2	adantr	⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → Ⅎ 𝑥 𝐵 )
20	6 9 15 17 18 19	iota2df	⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ( 𝜒 ↔ ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) = 𝐵 ) )
21		df-riota	⊢ ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
22	21	eqeq1i	⊢ ( ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 ↔ ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) = 𝐵 )
23	20 22	bitr4di	⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ( 𝜒 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 ) )

Metamath Proof Explorer

Theorem riota2df

Proof