Metamath Proof Explorer


Theorem nfiundg

Description: Bound-variable hypothesis builder for indexed union. Usage of this theorem is discouraged because it depends on ax-13 , see nfiund for a weaker version that does not require it. (Contributed by Emmett Weisz, 6-Dec-2019) (New usage is discouraged.)

Ref Expression
Hypotheses nfiundg.1 𝑥 𝜑
nfiundg.2 ( 𝜑 𝑦 𝐴 )
nfiundg.3 ( 𝜑 𝑦 𝐵 )
Assertion nfiundg ( 𝜑 𝑦 𝑥𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 nfiundg.1 𝑥 𝜑
2 nfiundg.2 ( 𝜑 𝑦 𝐴 )
3 nfiundg.3 ( 𝜑 𝑦 𝐵 )
4 df-iun 𝑥𝐴 𝐵 = { 𝑧 ∣ ∃ 𝑥𝐴 𝑧𝐵 }
5 nfv 𝑧 𝜑
6 3 nfcrd ( 𝜑 → Ⅎ 𝑦 𝑧𝐵 )
7 1 2 6 nfrexdg ( 𝜑 → Ⅎ 𝑦𝑥𝐴 𝑧𝐵 )
8 5 7 nfabd ( 𝜑 𝑦 { 𝑧 ∣ ∃ 𝑥𝐴 𝑧𝐵 } )
9 4 8 nfcxfrd ( 𝜑 𝑦 𝑥𝐴 𝐵 )