Theorem en3i

Description: Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 19-Jul-2004)

	Ref	Expression
Hypotheses	en3i.1	⊢ 𝐴 ∈ V
	en3i.2	⊢ 𝐵 ∈ V
	en3i.3	⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 )
	en3i.4	⊢ ( 𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴 )
	en3i.5	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 = 𝐷 ↔ 𝑦 = 𝐶 ) )
Assertion	en3i	⊢ 𝐴 ≈ 𝐵

Proof

Step	Hyp	Ref	Expression
1		en3i.1	⊢ 𝐴 ∈ V
2		en3i.2	⊢ 𝐵 ∈ V
3		en3i.3	⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 )
4		en3i.4	⊢ ( 𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴 )
5		en3i.5	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 = 𝐷 ↔ 𝑦 = 𝐶 ) )
6	1	a1i	⊢ ( ⊤ → 𝐴 ∈ V )
7	2	a1i	⊢ ( ⊤ → 𝐵 ∈ V )
8	3	a1i	⊢ ( ⊤ → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )
9	4	a1i	⊢ ( ⊤ → ( 𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴 ) )
10	5	a1i	⊢ ( ⊤ → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 = 𝐷 ↔ 𝑦 = 𝐶 ) ) )
11	6 7 8 9 10	en3d	⊢ ( ⊤ → 𝐴 ≈ 𝐵 )
12	11	mptru	⊢ 𝐴 ≈ 𝐵