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

Metamath Proof Explorer

Theorem bnj985v

Description: Version of bnj985 with an additional disjoint variable condition, not requiring ax-13 . (Contributed by GG, 27-Mar-2024) (New usage is discouraged.)

Ref Expression
Hypotheses bnj985v.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
bnj985v.6 ⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 )
bnj985v.9 ⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ )
bnj985v.11 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
bnj985v.13 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
Assertion bnj985v ( 𝐺 ∈ 𝐵 ↔ ∃ 𝑝 𝜒″ )

Proof

Step Hyp Ref Expression
1 bnj985v.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
2 bnj985v.6 ⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 )
3 bnj985v.9 ⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ )
4 bnj985v.11 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
5 bnj985v.13 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
6 5 bnj918 ⊢ 𝐺 ∈ V
7 1 4 bnj984 ⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ 𝐵 ↔ [ 𝐺 / 𝑓 ] ∃ 𝑛 𝜒 ) )
8 6 7 ax-mp ⊢ ( 𝐺 ∈ 𝐵 ↔ [ 𝐺 / 𝑓 ] ∃ 𝑛 𝜒 )
9 sbcex2 ⊢ ( [ 𝐺 / 𝑓 ] ∃ 𝑝 𝜒′ ↔ ∃ 𝑝 [ 𝐺 / 𝑓 ] 𝜒′ )
10 nfv ⊢ Ⅎ 𝑝 𝜒
11 10 sb8ef ⊢ ( ∃ 𝑛 𝜒 ↔ ∃ 𝑝 [ 𝑝 / 𝑛 ] 𝜒 )
12 sbsbc ⊢ ( [ 𝑝 / 𝑛 ] 𝜒 ↔ [ 𝑝 / 𝑛 ] 𝜒 )
13 12 exbii ⊢ ( ∃ 𝑝 [ 𝑝 / 𝑛 ] 𝜒 ↔ ∃ 𝑝 [ 𝑝 / 𝑛 ] 𝜒 )
14 11 13 bitri ⊢ ( ∃ 𝑛 𝜒 ↔ ∃ 𝑝 [ 𝑝 / 𝑛 ] 𝜒 )
15 14 2 bnj133 ⊢ ( ∃ 𝑛 𝜒 ↔ ∃ 𝑝 𝜒′ )
16 15 sbcbii ⊢ ( [ 𝐺 / 𝑓 ] ∃ 𝑛 𝜒 ↔ [ 𝐺 / 𝑓 ] ∃ 𝑝 𝜒′ )
17 3 exbii ⊢ ( ∃ 𝑝 𝜒″ ↔ ∃ 𝑝 [ 𝐺 / 𝑓 ] 𝜒′ )
18 9 16 17 3bitr4i ⊢ ( [ 𝐺 / 𝑓 ] ∃ 𝑛 𝜒 ↔ ∃ 𝑝 𝜒″ )
19 8 18 bitri ⊢ ( 𝐺 ∈ 𝐵 ↔ ∃ 𝑝 𝜒″ )