Metamath Proof Explorer


Theorem iinexg

Description: The existence of a class intersection. x is normally a free-variable parameter in B , which should be read B ( x ) . (Contributed by FL, 19-Sep-2011)

Ref Expression
Assertion iinexg ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥𝐴 𝐵𝐶 ) → 𝑥𝐴 𝐵 ∈ V )

Proof

Step Hyp Ref Expression
1 dfiin2g ( ∀ 𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } )
2 1 adantl ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥𝐴 𝐵𝐶 ) → 𝑥𝐴 𝐵 = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } )
3 elisset ( 𝐵𝐶 → ∃ 𝑦 𝑦 = 𝐵 )
4 3 rgenw 𝑥𝐴 ( 𝐵𝐶 → ∃ 𝑦 𝑦 = 𝐵 )
5 r19.2z ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥𝐴 ( 𝐵𝐶 → ∃ 𝑦 𝑦 = 𝐵 ) ) → ∃ 𝑥𝐴 ( 𝐵𝐶 → ∃ 𝑦 𝑦 = 𝐵 ) )
6 4 5 mpan2 ( 𝐴 ≠ ∅ → ∃ 𝑥𝐴 ( 𝐵𝐶 → ∃ 𝑦 𝑦 = 𝐵 ) )
7 r19.35 ( ∃ 𝑥𝐴 ( 𝐵𝐶 → ∃ 𝑦 𝑦 = 𝐵 ) ↔ ( ∀ 𝑥𝐴 𝐵𝐶 → ∃ 𝑥𝐴𝑦 𝑦 = 𝐵 ) )
8 6 7 sylib ( 𝐴 ≠ ∅ → ( ∀ 𝑥𝐴 𝐵𝐶 → ∃ 𝑥𝐴𝑦 𝑦 = 𝐵 ) )
9 8 imp ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥𝐴 𝐵𝐶 ) → ∃ 𝑥𝐴𝑦 𝑦 = 𝐵 )
10 rexcom4 ( ∃ 𝑥𝐴𝑦 𝑦 = 𝐵 ↔ ∃ 𝑦𝑥𝐴 𝑦 = 𝐵 )
11 9 10 sylib ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥𝐴 𝐵𝐶 ) → ∃ 𝑦𝑥𝐴 𝑦 = 𝐵 )
12 abn0 ( { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } ≠ ∅ ↔ ∃ 𝑦𝑥𝐴 𝑦 = 𝐵 )
13 11 12 sylibr ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥𝐴 𝐵𝐶 ) → { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } ≠ ∅ )
14 intex ( { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } ≠ ∅ ↔ { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } ∈ V )
15 13 14 sylib ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥𝐴 𝐵𝐶 ) → { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } ∈ V )
16 2 15 eqeltrd ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥𝐴 𝐵𝐶 ) → 𝑥𝐴 𝐵 ∈ V )