Theorem bj-inex1gALT 37504

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

Assertion

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

Proof of Theorem bj-inex1gALT

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sepg 5258	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
2		dfcleq 2754	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
3		elin 3920	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
4	3	a1i 11	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
5	4	bibi2d 345	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))))
6	5	albidv 1948	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))))
7	2, 6	bitrid 286	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))))
8	7	exbidv 1949	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))))
9	1, 8	mpbird 260	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = (𝐴 ∩ 𝐵))
10		isset 3467	. 2 ⊢ ((𝐴 ∩ 𝐵) ∈ V ↔ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵))
11	9, 10	sylibr 237	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1566   = wceq 1568  ∃wex 1807   ∈ wcel 2141  Vcvv 3453   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5256

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3911

This theorem is referenced by: (None)