Theorem bj-inex1gALT 38014

Description: Proof of inex1g 5283 from sepg 5254 to then allow proving inex1 5281 from it. That does not reduce the combined proof size of inex1 5281 and inex1g 5283. (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 5254	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
2		dfcleq 2756	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
3		elin 4096	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
4	3	a1i 11	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
5	4	bibi2d 345	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))))
6	5	albidv 1955	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))))
7	2, 6	bitrid 286	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))))
8	7	exbidv 1956	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))))
9	1, 8	mpbird 260	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = (𝐴 ∩ 𝐵))
10		isset 3468	. 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 2147  Vcvv 3454   ∩ cin 4092

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094

This theorem is used by: (None)