Theorem nfopab1 5177

Description: The first abstraction variable in an ordered-pair class abstraction is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)

Assertion

Ref	Expression
nfopab1	⊢ Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}

Proof of Theorem nfopab1

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-opab 5170	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
2		nfe1 2189	. . 3 ⊢ Ⅎ𝑥∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
3	2	nfab 2931	. 2 ⊢ Ⅎ𝑥{𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
4	1, 3	nfcxfr 2923	1 ⊢ Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569  ∃wex 1811  {cab 2741  Ⅎwnfc 2910  ⟨cop 4837  {copab 5169

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-opab 5170

This theorem is used by:  nfmpt1  5206  rexopabb  5505  ssopab2bw  5525  ssopab2b  5527  dmopab  5901  rnopab  5940  funopab  6583  fvopab5  7035  zfrep6OLD  7974  opabdm  33259  opabrn  33260  fpwrelmap  33378  rankse  35802  fineqvrep  35853  srepdflem2  36040  bj-opabco  38249  vvdifopab  39337  aomclem8  44203  sprsymrelf  48716