Metamath Proof Explorer


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 ( 𝜑 𝑥𝐴 , 𝐵 ⟩ )