Theorem nfopdALT

Description: Deduction version of bound-variable hypothesis builder nfop . This shows how the deduction version of a not-free theorem such as nfop can be created from the corresponding not-free inference theorem. (Contributed by NM, 19-Nov-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfopdALT.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
	nfopdALT.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
Assertion	nfopdALT	⊢ ( 𝜑 → Ⅎ 𝑥 ⟨ 𝐴 , 𝐵 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		nfopdALT.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2		nfopdALT.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
3		abidnf	⊢ ( Ⅎ 𝑥 𝐴 → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } = 𝐴 )
4	3	adantr	⊢ ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝐵 ) → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } = 𝐴 )
5		abidnf	⊢ ( Ⅎ 𝑥 𝐵 → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } = 𝐵 )
6	5	adantl	⊢ ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝐵 ) → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } = 𝐵 )
7	4 6	opeq12d	⊢ ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝐵 ) → ⟨ { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } , { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
8		nfaba1	⊢ Ⅎ 𝑥 { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 }
9		nfaba1	⊢ Ⅎ 𝑥 { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 }
10	8 9	nfop	⊢ Ⅎ 𝑥 ⟨ { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } , { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } ⟩
11	1 2 7 10	nfded2	⊢ ( 𝜑 → Ⅎ 𝑥 ⟨ 𝐴 , 𝐵 ⟩ )