Theorem bj-inex1gALT 37837

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144  Vcvv 3450   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4091

This theorem is used by: (None)