Theorem elrnmpo 7560

Description: Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)

Hypotheses

Ref	Expression
rngop.1	⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
elrnmpo.1	⊢ 𝐶 ∈ V

Assertion

Ref	Expression
elrnmpo	⊢ (𝐷 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶)

Distinct variable groups:   𝑦,𝐴   𝑥,𝑦,𝐷

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥, 𝑦)   𝐶(𝑥, 𝑦)   𝐹(𝑥, 𝑦)

Proof of Theorem elrnmpo

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rngop.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
2	1	rnmpo 7557	. . 3 ⊢ ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶}
3	2	eleq2i 2852	. 2 ⊢ (𝐷 ∈ ran 𝐹 ↔ 𝐷 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶})
4		elrnmpo.1	. . . . . 6 ⊢ 𝐶 ∈ V
5		eleq1 2848	. . . . . 6 ⊢ (𝐷 = 𝐶 → (𝐷 ∈ V ↔ 𝐶 ∈ V))
6	4, 5	mpbiri 261	. . . . 5 ⊢ (𝐷 = 𝐶 → 𝐷 ∈ V)
7	6	rexlimivw 3159	. . . 4 ⊢ (∃𝑦 ∈ 𝐵 𝐷 = 𝐶 → 𝐷 ∈ V)
8	7	rexlimivw 3159	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶 → 𝐷 ∈ V)
9		eqeq1 2764	. . . 4 ⊢ (𝑧 = 𝐷 → (𝑧 = 𝐶 ↔ 𝐷 = 𝐶))
10	9	2rexbidv 3227	. . 3 ⊢ (𝑧 = 𝐷 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶))
11	8, 10	elab3 3639	. 2 ⊢ (𝐷 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶)
12	3, 11	bitri 278	1 ⊢ (𝐷 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ∈ wcel 2144  {cab 2738  ∃wrex 3086  Vcvv 3450  ran crn 5652   ∈ cmpo 7426

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 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-cnv 5659  df-dm 5661  df-rn 5662  df-oprab 7428  df-mpo 7429

This theorem is used by:  qexALT  13098  lsmelvalx  19863  efgtlen  19949  frgpnabllem1  20096  fmucndlem  24618  mbfimaopnlem  25985  tglnunirn  29020  isplng  29265  tpr2rico  34594  mbfmco2  34947  br2base  34951  dya2icobrsiga  34958  dya2iocnrect  34963  dya2iocucvr  34966  sxbrsigalem2  34968  cntotbnd  38867  eldiophb  43905  elicores  46681  volicorescl  47699