This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfdisjw

Description: Bound-variable hypothesis builder for disjoint collection. Version of nfdisj with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 14-Nov-2016) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

Ref Expression
Hypotheses nfdisjw.1 ⊢ Ⅎ 𝑦 𝐴
nfdisjw.2 ⊢ Ⅎ 𝑦 𝐵
Assertion nfdisjw Ⅎ 𝑦 Disj 𝑥 ∈ 𝐴 𝐵

Proof

Step Hyp Ref Expression
1 nfdisjw.1 ⊢ Ⅎ 𝑦 𝐴
2 nfdisjw.2 ⊢ Ⅎ 𝑦 𝐵
3 dfdisj2 ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑧 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
4 nftru ⊢ Ⅎ 𝑥 ⊤
5 nfcvd ⊢ ( ⊤ → Ⅎ 𝑦 𝑥 )
6 1 a1i ⊢ ( ⊤ → Ⅎ 𝑦 𝐴 )
7 5 6 nfeld ⊢ ( ⊤ → Ⅎ 𝑦 𝑥 ∈ 𝐴 )
8 2 nfcri ⊢ Ⅎ 𝑦 𝑧 ∈ 𝐵
9 8 a1i ⊢ ( ⊤ → Ⅎ 𝑦 𝑧 ∈ 𝐵 )
10 7 9 nfand ⊢ ( ⊤ → Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
11 4 10 nfmodv ⊢ ( ⊤ → Ⅎ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
12 11 mptru ⊢ Ⅎ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 )
13 12 nfal ⊢ Ⅎ 𝑦 ∀ 𝑧 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 )
14 3 13 nfxfr ⊢ Ⅎ 𝑦 Disj 𝑥 ∈ 𝐴 𝐵