Theorem bj-inex1gALT

Description: Proof of inex1g from sepg to then allow proving inex1 from it. That does not reduce the combined proof size of inex1 and inex1g . (Contributed by BJ, 14-Jul-2026) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-inex1gALT	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		sepg	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
2		dfcleq	⊢ ( 𝑥 = ( 𝐴 ∩ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) )
3		elin	⊢ ( 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
4	3	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
5	4	bibi2d	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) )
6	5	albidv	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) )
7	2 6	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 = ( 𝐴 ∩ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) )
8	7	exbidv	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 𝑥 = ( 𝐴 ∩ 𝐵 ) ↔ ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) )
9	1 8	mpbird	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = ( 𝐴 ∩ 𝐵 ) )
10		isset	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ V ↔ ∃ 𝑥 𝑥 = ( 𝐴 ∩ 𝐵 ) )
11	9 10	sylibr	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ 𝐵 ) ∈ V )