Metamath Proof Explorer


Theorem bnj985v

Description: Version of bnj985 with an additional disjoint variable condition, not requiring ax-13 . (Contributed by Gino Giotto, 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 sb8ev ( ∃ 𝑛 𝜒 ↔ ∃ 𝑝 [ 𝑝 / 𝑛 ] 𝜒 )
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 ( 𝐺𝐵 ↔ ∃ 𝑝 𝜒″ )