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

Metamath Proof Explorer

Theorem nfdisj

Description: Bound-variable hypothesis builder for disjoint collection. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfdisjw when possible. (Contributed by Mario Carneiro, 14-Nov-2016) (New usage is discouraged.)

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

Proof

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