Theorem en2i

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

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

Proof

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