Theorem bj-inex1gALT 37655

Description: Proof of inex1g 5286 from sepg 5257 to then allow proving inex1 5284 from it. That does not reduce the combined proof size of inex1 5284 and inex1g 5286. (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 5257	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
2		dfcleq 2755	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
3		elin 3918	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
4	3	a1i 11	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
5	4	bibi2d 345	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))))
6	5	albidv 1953	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))))
7	2, 6	bitrid 286	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))))
8	7	exbidv 1954	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))))
9	1, 8	mpbird 260	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = (𝐴 ∩ 𝐵))
10		isset 3467	. 2 ⊢ ((𝐴 ∩ 𝐵) ∈ V ↔ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵))
11	9, 10	sylibr 237	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3453   ∩ cin 3901

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-in 3909

This theorem is used by: (None)